Language.Syntactic.Features.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.Features.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

WitnessSat (Tuple ctx)

WitnessCons (Tuple ctx)

ExprEq (Tuple ctx)

ToTree (Tuple ctx)

Render (Tuple ctx)

Eval (Tuple ctx)

IsSymbol (Tuple ctx)

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

prjTuple :: (Tuple ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Tuple ctx a)

Partial Tuple projection with explicit context

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

data Select ctx a where

Expressions for selecting elements of a tuple

Constructors

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

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

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

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

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

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

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

Instances

WitnessSat (Select ctx)

WitnessCons (Select ctx)

ExprEq (Select ctx)

ToTree (Select ctx)

Render (Select ctx)

Eval (Select ctx)

IsSymbol (Select ctx)

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

prjSelect :: (Select ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Select ctx a)

Partial Select projection with explicit context

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)