Language.Syntactic.Constructs.Tuple

Construction and projection of tuples in the object language

The function pairs desugarTupX/sugarTupX could be used directly in Syntactic instances if it wasn't for the extra (Proxy ctx) arguments. For this reason, Syntactic instances have to be written manually for each context. The module Language.Syntactic.Constructs.TupleSyntacticPoly provides instances for a Poly context. The exact same code can be used to make instances for other contexts -- just copy/paste and replace Poly and poly with the desired context (and probably add an extra constraint in the class contexts).

Construction

data Tuple ctx a where

Expressions for constructing tuples

Constructors

Tup2 :: Sat ctx (a, b) => Tuple ctx (a :-> (b :-> Full (a, b)))

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

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

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

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

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

Instances

MaybeWitnessSat ctx1 (Tuple ctx2)

MaybeWitnessSat ctx (Tuple ctx)

WitnessSat (Tuple ctx)

WitnessCons (Tuple ctx)

ExprEq (Tuple ctx)

ToTree (Tuple ctx)

Render (Tuple ctx)

Eval (Tuple ctx)

Semantic (Tuple ctx)

EvalBind (Tuple ctx)

(:<: (Tuple ctx') dom, Optimize dom ctx dom) => Optimize (Tuple ctx') ctx dom

AlphaEq dom dom dom env => AlphaEq (Tuple ctx) (Tuple ctx) dom env

desugarTup2 :: (Syntactic a dom, Syntactic b dom, Sat ctx (Internal a, Internal b), Tuple ctx :<: dom) => Proxy ctx -> (a, b) -> ASTF dom (Internal a, Internal b)

desugarTup3 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Sat ctx (Internal a, Internal b, Internal c), Tuple ctx :<: dom) => Proxy ctx -> (a, b, c) -> ASTF dom (Internal a, Internal b, Internal c)

desugarTup4 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Sat ctx (Internal a, Internal b, Internal c, Internal d), Tuple ctx :<: dom) => Proxy ctx -> (a, b, c, d) -> ASTF dom (Internal a, Internal b, Internal c, Internal d)

desugarTup5 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e), Tuple ctx :<: dom) => Proxy ctx -> (a, b, c, d, e) -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)

desugarTup6 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f), Tuple ctx :<: dom) => Proxy ctx -> (a, b, c, d, e, f) -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)

desugarTup7 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Syntactic g dom, Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g), Tuple ctx :<: dom) => Proxy ctx -> (a, b, c, d, e, f, g) -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)

Projection

type family Sel1' a

These families (Sel1' - Sel7') 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

data Select ctx a where

Expressions for selecting elements of a tuple

Constructors

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

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

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

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

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

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

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

Instances

MaybeWitnessSat ctx1 (Select ctx2)

MaybeWitnessSat ctx (Select ctx)

WitnessSat (Select ctx)

WitnessCons (Select ctx)

ExprEq (Select ctx)

ToTree (Select ctx)

Render (Select ctx)

Eval (Select ctx)

Semantic (Select ctx)

EvalBind (Select ctx)

(:<: (Select ctx') dom, Optimize dom ctx dom) => Optimize (Select ctx') ctx dom

AlphaEq dom dom dom env => AlphaEq (Select ctx) (Select ctx) dom env

selectPos :: Select ctx a -> Int

Return the selected position, e.g.

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

sugarTup2 :: (Syntactic a dom, Syntactic b dom, Sat ctx (Internal a), Sat ctx (Internal b), Select ctx :<: dom) => Proxy ctx -> ASTF dom (Internal a, Internal b) -> (a, b)

sugarTup3 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Select ctx :<: dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c) -> (a, b, c)

sugarTup4 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), Select ctx :<: dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d) -> (a, b, c, d)

sugarTup5 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), Sat ctx (Internal e), Select ctx :<: dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e) -> (a, b, c, d, e)

sugarTup6 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), Sat ctx (Internal e), Sat ctx (Internal f), Select ctx :<: dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f) -> (a, b, c, d, e, f)

sugarTup7 :: (Syntactic a dom, Syntactic b dom, Syntactic c dom, Syntactic d dom, Syntactic e dom, Syntactic f dom, Syntactic g dom, Sat ctx (Internal a), Sat ctx (Internal b), Sat ctx (Internal c), Sat ctx (Internal d), Sat ctx (Internal e), Sat ctx (Internal f), Sat ctx (Internal g), Select ctx :<: dom) => Proxy ctx -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g) -> (a, b, c, d, e, f, g)