{-# LANGUAGE DefaultSignatures #-}

module Language.Hasmtlib.Iteable where

import Language.Hasmtlib.Internal.Expr
import Data.Sequence (Seq)
import Data.Tree
  
-- | If condition (p :: b) then (t :: a) else (f :: a)
--   
--    >>> ite true "1" "2"
--        "1"
--    >>> ite false 100 42
--        42 
class Iteable b a where
  ite :: b -> a -> a -> a
  default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a
  ite b
p a
t a
f = (c -> c -> c) -> f c -> f c -> f c
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (b -> c -> c -> c
forall b a. Iteable b a => b -> a -> a -> a
ite b
p) a
f c
t a
f c
f

instance Iteable (Expr BoolSort) (Expr t) where
  ite :: Expr 'BoolSort -> Expr t -> Expr t -> Expr t
ite = Expr 'BoolSort -> Expr t -> Expr t -> Expr t
forall (t :: SMTSort). Expr 'BoolSort -> Expr t -> Expr t -> Expr t
Ite
  {-# INLINE ite #-}

instance Iteable Bool a where
  ite :: Bool -> a -> a -> a
ite Bool
p a
t a
f = if Bool
p then a
t else a
f
  {-# INLINE ite #-}

instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) [a]
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Maybe a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Seq a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Tree a)

instance Iteable (Expr BoolSort) () where
  ite :: Expr 'BoolSort -> () -> () -> ()
ite Expr 'BoolSort
_ ()
_ ()
_ = ()

instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b) => Iteable (Expr BoolSort) (a,b) where
  ite :: Expr 'BoolSort -> (a, b) -> (a, b) -> (a, b)
ite Expr 'BoolSort
p (a
a,b
b) (a
a',b
b') = (Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p a
a a
a', Expr 'BoolSort -> b -> b -> b
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p b
b b
b')

instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c) => Iteable (Expr BoolSort) (a,b,c) where
  ite :: Expr 'BoolSort -> (a, b, c) -> (a, b, c) -> (a, b, c)
ite Expr 'BoolSort
p (a
a,b
b,c
c) (a
a',b
b',c
c') = (Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p a
a a
a', Expr 'BoolSort -> b -> b -> b
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p b
b b
b', Expr 'BoolSort -> c -> c -> c
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p c
c c
c')
  
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d) => Iteable (Expr BoolSort) (a,b,c,d) where
  ite :: Expr 'BoolSort -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d)
ite Expr 'BoolSort
p (a
a,b
b,c
c,d
d) (a
a',b
b',c
c',d
d') = (Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p a
a a
a', Expr 'BoolSort -> b -> b -> b
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p b
b b
b', Expr 'BoolSort -> c -> c -> c
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p c
c c
c', Expr 'BoolSort -> d -> d -> d
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p d
d d
d')
  
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e) => Iteable (Expr BoolSort) (a,b,c,d,e) where
  ite :: Expr 'BoolSort
-> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e)
ite Expr 'BoolSort
p (a
a,b
b,c
c,d
d,e
e) (a
a',b
b',c
c',d
d',e
e') = (Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p a
a a
a', Expr 'BoolSort -> b -> b -> b
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p b
b b
b', Expr 'BoolSort -> c -> c -> c
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p c
c c
c', Expr 'BoolSort -> d -> d -> d
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p d
d d
d', Expr 'BoolSort -> e -> e -> e
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p e
e e
e')
  
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f) => Iteable (Expr BoolSort) (a,b,c,d,e,f) where
  ite :: Expr 'BoolSort
-> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)
ite Expr 'BoolSort
p (a
a,b
b,c
c,d
d,e
e,f
f) (a
a',b
b',c
c',d
d',e
e',f
f') = (Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p a
a a
a', Expr 'BoolSort -> b -> b -> b
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p b
b b
b', Expr 'BoolSort -> c -> c -> c
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p c
c c
c', Expr 'BoolSort -> d -> d -> d
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p d
d d
d', Expr 'BoolSort -> e -> e -> e
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p e
e e
e', Expr 'BoolSort -> f -> f -> f
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p f
f f
f')
  
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g) where
  ite :: Expr 'BoolSort
-> (a, b, c, d, e, f, g)
-> (a, b, c, d, e, f, g)
-> (a, b, c, d, e, f, g)
ite Expr 'BoolSort
p (a
a,b
b,c
c,d
d,e
e,f
f,g
g) (a
a',b
b',c
c',d
d',e
e',f
f',g
g') = (Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p a
a a
a', Expr 'BoolSort -> b -> b -> b
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p b
b b
b', Expr 'BoolSort -> c -> c -> c
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p c
c c
c', Expr 'BoolSort -> d -> d -> d
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p d
d d
d', Expr 'BoolSort -> e -> e -> e
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p e
e e
e', Expr 'BoolSort -> f -> f -> f
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p f
f f
f', Expr 'BoolSort -> g -> g -> g
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p g
g g
g')  
  
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g, Iteable (Expr BoolSort) h) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g,h) where
  ite :: Expr 'BoolSort
-> (a, b, c, d, e, f, g, h)
-> (a, b, c, d, e, f, g, h)
-> (a, b, c, d, e, f, g, h)
ite Expr 'BoolSort
p (a
a,b
b,c
c,d
d,e
e,f
f,g
g,h
h) (a
a',b
b',c
c',d
d',e
e',f
f',g
g',h
h') = (Expr 'BoolSort -> a -> a -> a
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p a
a a
a', Expr 'BoolSort -> b -> b -> b
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p b
b b
b', Expr 'BoolSort -> c -> c -> c
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p c
c c
c', Expr 'BoolSort -> d -> d -> d
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p d
d d
d', Expr 'BoolSort -> e -> e -> e
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p e
e e
e', Expr 'BoolSort -> f -> f -> f
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p f
f f
f', Expr 'BoolSort -> g -> g -> g
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p g
g g
g', Expr 'BoolSort -> h -> h -> h
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p h
h h
h')