Language.Syntactic.Constructs.Tuple

Construction and elimination of tuples in the object language

Construction

data Tuple sig where

Expressions for constructing tuples

Constructors

Tup2 :: Tuple (a :-> (b :-> Full (a, b)))

Tup3 :: Tuple (a :-> (b :-> (c :-> Full (a, b, c))))

Tup4 :: Tuple (a :-> (b :-> (c :-> (d :-> Full (a, b, c, d)))))

Tup5 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> Full (a, b, c, d, e))))))

Tup6 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> Full (a, b, c, d, e, f)))))))

Tup7 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> Full (a, b, c, d, e, f, g))))))))

Tup8 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> Full (a, b, c, d, e, f, g, h)))))))))

Tup9 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> Full (a, b, c, d, e, f, g, h, i))))))))))

Tup10 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> Full (a, b, c, d, e, f, g, h, i, j)))))))))))

Tup11 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> Full (a, b, c, d, e, f, g, h, i, j, k))))))))))))

Tup12 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> Full (a, b, c, d, e, f, g, h, i, j, k, l)))))))))))))

Tup13 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> (m :-> Full (a, b, c, d, e, f, g, h, i, j, k, l, m))))))))))))))

Tup14 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> (m :-> (n :-> Full (a, b, c, d, e, f, g, h, i, j, k, l, m, n)))))))))))))))

Tup15 :: Tuple (a :-> (b :-> (c :-> (d :-> (e :-> (f :-> (g :-> (h :-> (i :-> (j :-> (k :-> (l :-> (m :-> (n :-> (o :-> Full (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o))))))))))))))))

Instances

Equality Tuple

StringTree Tuple

Render Tuple

Eval Tuple

Semantic Tuple

Constrained Tuple

EvalBind Tuple

Optimize Tuple

AlphaEq dom dom dom env => AlphaEq Tuple Tuple dom env

TupleSat (:+: (:|| Tuple p) dom2) p

TupleSat (:|| Tuple p) p

Projection

type family Sel1' a

These families (Sel1' - Sel15') are needed because of the problem described in:

http://emil-fp.blogspot.com/2011/08/fundeps-weaker-than-type-families.html

type family Sel2' a

type family Sel3' a

type family Sel4' a

type family Sel5' a

type family Sel6' a

type family Sel7' a

type family Sel8' a

type family Sel9' a

type family Sel10' a

type family Sel11' a

type family Sel12' a

type family Sel13' a

type family Sel14' a

type family Sel15' a

data Select a where

Expressions for selecting elements of a tuple

Constructors

Sel1 :: (Sel1 a b, Sel1' a ~ b) => Select (a :-> Full b)

Sel2 :: (Sel2 a b, Sel2' a ~ b) => Select (a :-> Full b)

Sel3 :: (Sel3 a b, Sel3' a ~ b) => Select (a :-> Full b)

Sel4 :: (Sel4 a b, Sel4' a ~ b) => Select (a :-> Full b)

Sel5 :: (Sel5 a b, Sel5' a ~ b) => Select (a :-> Full b)

Sel6 :: (Sel6 a b, Sel6' a ~ b) => Select (a :-> Full b)

Sel7 :: (Sel7 a b, Sel7' a ~ b) => Select (a :-> Full b)

Sel8 :: (Sel8 a b, Sel8' a ~ b) => Select (a :-> Full b)

Sel9 :: (Sel9 a b, Sel9' a ~ b) => Select (a :-> Full b)

Sel10 :: (Sel10 a b, Sel10' a ~ b) => Select (a :-> Full b)

Sel11 :: (Sel11 a b, Sel11' a ~ b) => Select (a :-> Full b)

Sel12 :: (Sel12 a b, Sel12' a ~ b) => Select (a :-> Full b)

Sel13 :: (Sel13 a b, Sel13' a ~ b) => Select (a :-> Full b)

Sel14 :: (Sel14 a b, Sel14' a ~ b) => Select (a :-> Full b)

Sel15 :: (Sel15 a b, Sel15' a ~ b) => Select (a :-> Full b)

Instances

Equality Select

StringTree Select

Render Select

Eval Select

Semantic Select

Constrained Select

EvalBind Select

Optimize Select

AlphaEq dom dom dom env => AlphaEq Select Select dom env

TupleSat (:+: (:|| Select p) dom2) p

TupleSat (:|| Select p) p

selectPos :: Select a -> Int

Return the selected position, e.g.

 selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3