module Language.Syntactic.Constructs.Tuple where
import Data.Proxy
import Data.Tuple.Curry
import Data.Tuple.Select
import Language.Syntactic
import Language.Syntactic.Interpretation.Semantics
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))
instance WitnessCons (Tuple ctx)
where
witnessCons Tup2 = ConsWit
witnessCons Tup3 = ConsWit
witnessCons Tup4 = ConsWit
witnessCons Tup5 = ConsWit
witnessCons Tup6 = ConsWit
witnessCons Tup7 = ConsWit
instance WitnessSat (Tuple ctx)
where
type SatContext (Tuple ctx) = ctx
witnessSat Tup2 = SatWit
witnessSat Tup3 = SatWit
witnessSat Tup4 = SatWit
witnessSat Tup5 = SatWit
witnessSat Tup6 = SatWit
witnessSat Tup7 = SatWit
instance MaybeWitnessSat ctx (Tuple ctx)
where
maybeWitnessSat = maybeWitnessSatDefault
instance MaybeWitnessSat ctx1 (Tuple ctx2)
where
maybeWitnessSat _ _ = Nothing
instance Semantic (Tuple ctx)
where
semantics Tup2 = Sem "tup2" (,)
semantics Tup3 = Sem "tup3" (,,)
semantics Tup4 = Sem "tup4" (,,,)
semantics Tup5 = Sem "tup5" (,,,,)
semantics Tup6 = Sem "tup6" (,,,,,)
semantics Tup7 = Sem "tup7" (,,,,,,)
instance ExprEq (Tuple ctx) where exprEq = exprEqSem; exprHash = exprHashSem
instance Render (Tuple ctx) where renderPart = renderPartSem
instance Eval (Tuple ctx) where evaluate = evaluateSem
instance ToTree (Tuple ctx)
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)
desugarTup2 ctx = uncurryN $ sugarSymCtx ctx Tup2
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)
desugarTup3 ctx = uncurryN $ sugarSymCtx ctx Tup3
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)
desugarTup4 ctx = uncurryN $ sugarSymCtx ctx Tup4
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)
desugarTup5 ctx = uncurryN $ sugarSymCtx ctx Tup5
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)
desugarTup6 ctx = uncurryN $ sugarSymCtx ctx Tup6
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)
desugarTup7 ctx = uncurryN $ sugarSymCtx ctx Tup7
type family Sel1' a
type instance Sel1' (a,b) = a
type instance Sel1' (a,b,c) = a
type instance Sel1' (a,b,c,d) = a
type instance Sel1' (a,b,c,d,e) = a
type instance Sel1' (a,b,c,d,e,f) = a
type instance Sel1' (a,b,c,d,e,f,g) = a
type family Sel2' a
type instance Sel2' (a,b) = b
type instance Sel2' (a,b,c) = b
type instance Sel2' (a,b,c,d) = b
type instance Sel2' (a,b,c,d,e) = b
type instance Sel2' (a,b,c,d,e,f) = b
type instance Sel2' (a,b,c,d,e,f,g) = b
type family Sel3' a
type instance Sel3' (a,b,c) = c
type instance Sel3' (a,b,c,d) = c
type instance Sel3' (a,b,c,d,e) = c
type instance Sel3' (a,b,c,d,e,f) = c
type instance Sel3' (a,b,c,d,e,f,g) = c
type family Sel4' a
type instance Sel4' (a,b,c,d) = d
type instance Sel4' (a,b,c,d,e) = d
type instance Sel4' (a,b,c,d,e,f) = d
type instance Sel4' (a,b,c,d,e,f,g) = d
type family Sel5' a
type instance Sel5' (a,b,c,d,e) = e
type instance Sel5' (a,b,c,d,e,f) = e
type instance Sel5' (a,b,c,d,e,f,g) = e
type family Sel6' a
type instance Sel6' (a,b,c,d,e,f) = f
type instance Sel6' (a,b,c,d,e,f,g) = f
type family Sel7' a
type instance Sel7' (a,b,c,d,e,f,g) = g
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)
instance WitnessCons (Select ctx)
where
witnessCons Sel1 = ConsWit
witnessCons Sel2 = ConsWit
witnessCons Sel3 = ConsWit
witnessCons Sel4 = ConsWit
witnessCons Sel5 = ConsWit
witnessCons Sel6 = ConsWit
witnessCons Sel7 = ConsWit
instance WitnessSat (Select ctx)
where
type SatContext (Select ctx) = ctx
witnessSat Sel1 = SatWit
witnessSat Sel2 = SatWit
witnessSat Sel3 = SatWit
witnessSat Sel4 = SatWit
witnessSat Sel5 = SatWit
witnessSat Sel6 = SatWit
witnessSat Sel7 = SatWit
instance MaybeWitnessSat ctx (Select ctx)
where
maybeWitnessSat = maybeWitnessSatDefault
instance MaybeWitnessSat ctx1 (Select ctx2)
where
maybeWitnessSat _ _ = Nothing
instance Semantic (Select ctx)
where
semantics Sel1 = Sem "sel1" sel1
semantics Sel2 = Sem "sel2" sel2
semantics Sel3 = Sem "sel3" sel3
semantics Sel4 = Sem "sel4" sel4
semantics Sel5 = Sem "sel5" sel5
semantics Sel6 = Sem "sel6" sel6
semantics Sel7 = Sem "sel7" sel7
instance ExprEq (Select ctx) where exprEq = exprEqSem; exprHash = exprHashSem
instance Render (Select ctx) where renderPart = renderPartSem
instance Eval (Select ctx) where evaluate = evaluateSem
instance ToTree (Select ctx)
selectPos :: Select ctx a -> Int
selectPos Sel1 = 1
selectPos Sel2 = 2
selectPos Sel3 = 3
selectPos Sel4 = 4
selectPos Sel5 = 5
selectPos Sel6 = 6
selectPos Sel7 = 7
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)
sugarTup2 ctx a =
( sugarSymCtx ctx Sel1 a
, sugarSymCtx ctx Sel2 a
)
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)
sugarTup3 ctx a =
( sugarSymCtx ctx Sel1 a
, sugarSymCtx ctx Sel2 a
, sugarSymCtx ctx Sel3 a
)
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)
sugarTup4 ctx a =
( sugarSymCtx ctx Sel1 a
, sugarSymCtx ctx Sel2 a
, sugarSymCtx ctx Sel3 a
, sugarSymCtx ctx Sel4 a
)
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)
sugarTup5 ctx a =
( sugarSymCtx ctx Sel1 a
, sugarSymCtx ctx Sel2 a
, sugarSymCtx ctx Sel3 a
, sugarSymCtx ctx Sel4 a
, sugarSymCtx ctx Sel5 a
)
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)
sugarTup6 ctx a =
( sugarSymCtx ctx Sel1 a
, sugarSymCtx ctx Sel2 a
, sugarSymCtx ctx Sel3 a
, sugarSymCtx ctx Sel4 a
, sugarSymCtx ctx Sel5 a
, sugarSymCtx ctx Sel6 a
)
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)
sugarTup7 ctx a =
( sugarSymCtx ctx Sel1 a
, sugarSymCtx ctx Sel2 a
, sugarSymCtx ctx Sel3 a
, sugarSymCtx ctx Sel4 a
, sugarSymCtx ctx Sel5 a
, sugarSymCtx ctx Sel6 a
, sugarSymCtx ctx Sel7 a
)