Safe Haskell | None |
---|
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 (
arguments.
For this reason, Proxy
ctx)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).
- data Tuple ctx a where
- 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))))))))
- 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)
- type family Sel1' a
- 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
- 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)
- selectPos :: Select ctx a -> Int
- 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)
Construction
Expressions for constructing tuples
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)))))))) |
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)Source
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)Source
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)Source
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)Source
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)Source
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)Source
Projection
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
Expressions for selecting elements of a tuple
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) |
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 -> IntSource
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)Source
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)Source
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)Source
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)Source
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)Source
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)Source