{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Static.Common where
import Data.Constraint ((:-) (..), Class (..), Dict (..))
import Data.Kind (Constraint, Type)
import Data.Singletons.Prelude
import Data.Singletons.TH (genDefunSymbols, singletons)
type family TyCont r (a :: Type) where
TyCont r a = a -> r
genDefunSymbols [''TyCont]
type family TyCont2 r (a1 :: Type) (a2 :: Type) where
TyCont2 r a1 a2 = a1 -> a2 -> r
genDefunSymbols [''TyCont2]
type family TyCont3 r (a1 :: Type) (a2 :: Type) (a3 :: Type) where
TyCont3 r a1 a2 a3 = a1 -> a2 -> a3 -> r
genDefunSymbols [''TyCont3]
singletons [d|
ap :: (x -> y -> z) -> (x -> y) -> (x -> z)
ap f g x = f x (g x)
|]
newtype CxtW c a = CxtW { unCxtW :: c => a }
type family ConstrainList (cc :: [Constraint]) :: Constraint where
ConstrainList '[] = ()
ConstrainList (c ': cc) = (c, ConstrainList cc)
type family NullC (t :: k) :: Constraint where
NullC t = ()
genDefunSymbols [''NullC]
type family NullC2 (t :: k) (t' :: k') :: Constraint where
NullC2 t t' = ()
genDefunSymbols [''NullC2]
type family AndC c0 c1 :: Constraint where
AndC c0 c1 = (c0, c1)
genDefunSymbols [''AndC]
type AndC1 c0 c1 = ApSym2 (AndCSym0 .@#@$$$ c0) c1
type AndC2 c0 c1 = ApSym2 (ApSym0 .@#@$$$ (.@#@$$) AndCSym0 .@#@$$$ c0) c1
type family Class2 c0 c1 t t' where
Class2 c0 c1 t t' = Class (c0 @@ t @@ t') (c1 @@ t @@ t')
genDefunSymbols [''Class2]
singletons [d|
lookupKV :: Eq k => k -> [k] -> [v] -> Maybe (k, v)
lookupKV k [] [] = Nothing
lookupKV k (k':kk) (v':vv) = lookupKV_If k k' kk v' vv (k == k')
lookupKV_If :: Eq k => k -> k -> [k] -> v -> [v] -> Bool -> Maybe (k, v)
lookupKV_If k k' _ v' _ True = Just (k', v')
lookupKV_If k _ kk _ vv False = lookupKV k kk vv
|]
class (Fmap (FmapSym1 f) (LookupKV k kk vv) ~
LookupKV k kk (Fmap f vv))
=> ProofLookupKV f k (kk :: [kt]) vv where
instance
ProofLookupKV f k '[] '[]
instance
(ProofLookupKV_If f k k' kk v' vv (k == k'))
=> ProofLookupKV f (k :: kt) (k' ': kk) (v' ': vv)
class (Fmap (FmapSym1 f) (LookupKV_If k k' kk v' vv eq) ~
LookupKV_If k k' kk (f @@ v') (Fmap f vv) eq)
=> ProofLookupKV_If f (k :: kt) k' kk v' vv eq where
instance
ProofLookupKV_If f k k' kk v' vv 'True
instance
ProofLookupKV f k kk vv
=> ProofLookupKV_If f k k' kk v' vv 'False
data TMaybe (t :: Maybe k) where
TNothing :: TMaybe 'Nothing
TJust :: !t -> TMaybe ('Just t)
data TCTab (c :: kt ~> Type ~> Constraint) (kk :: [kt]) (vv :: [Type]) :: Type where
TCNil :: TCTab c '[] '[]
TCCons :: (c @@ k @@ v) => !(Sing (k :: kt)) -> !v -> !(TCTab c kk vv) -> TCTab c (k : kk) (v : vv)
type TCTab' c = TCTab (ConstSym1 (TyCon1 c))
type TTab = TCTab NullC2Sym0
data TCMaybe c (t :: Maybe (kt, Type)) where
TCNothing :: TCMaybe c 'Nothing
TCJust :: Dict (c @@ k @@ v) -> !(Sing k) -> !v -> TCMaybe c ('Just '(k, v))
lookupTC
:: forall kt c f (k :: kt) (kk :: [kt]) vv
. SEq kt
=> Sing k
-> TCTab c kk vv
-> (TCMaybe c (LookupKV k kk vv), Dict (ProofLookupKV f k kk vv))
lookupTC k TCNil = (TCNothing, Dict)
lookupTC k (TCCons k' v tab) = case k %== k' of
STrue -> (TCJust Dict k' v, Dict)
SFalse -> case lookupTC @kt @c @f k tab of
(res, Dict) -> (res, Dict)
lookupTC2
:: forall kt c0 c1 f (k :: kt) (kk :: [kt]) vv
. SEq kt
=> Sing k
-> TCTab c0 kk vv
-> TCTab c1 kk (Fmap f vv)
-> ( TCMaybe c0 (LookupKV k kk vv)
, TCMaybe c1 (Fmap (FmapSym1 f) (LookupKV k kk vv))
)
lookupTC2 k TCNil TCNil = (TCNothing, TCNothing)
lookupTC2 k (TCCons k' v tab) (TCCons k'' p post) = case k %== k' of
STrue -> (TCJust Dict k' v, TCJust Dict k'' p)
SFalse -> lookupTC2 @kt @c0 @c1 @f k tab post
zipWithTC
:: forall kt c0 c1 cr f1 r (kk :: [kt]) vv
. TCTab c0 kk vv
-> TCTab c1 kk (Fmap f1 vv)
-> ( forall k0 k1 v
. (c0 @@ k0 @@ v)
=> (c1 @@ k1 @@ (f1 @@ v))
=> Sing k0
-> v
-> Sing k1
-> (f1 @@ v)
-> (r @@ v, Dict (cr @@ k0 @@ (r @@ v)))
)
-> TCTab cr kk (Fmap r vv)
zipWithTC TCNil TCNil f = TCNil
zipWithTC (TCCons k0 v t0) (TCCons k1 f1v t1) f = case f k0 v k1 f1v of
(v', Dict) -> TCCons k0 v' (zipWithTC @kt @c0 @c1 @cr @f1 @r t0 t1 f)
zipWith3TC
:: forall kt c0 c1 c2 cr f1 f2 r (kk :: [kt]) vv
. TCTab c0 kk vv
-> TCTab c1 kk (Fmap f1 vv)
-> TCTab c2 kk (Fmap f2 vv)
-> ( forall k0 k1 k2 v
. (c0 @@ k0 @@ v)
=> (c1 @@ k1 @@ (f1 @@ v))
=> (c2 @@ k2 @@ (f2 @@ v))
=> Sing k0 -> v
-> Sing k1 -> f1 @@ v
-> Sing k2 -> f2 @@ v
-> (r @@ v, Dict (cr @@ k0 @@ (r @@ v)))
)
-> TCTab cr kk (Fmap r vv)
zipWith3TC TCNil TCNil TCNil f = TCNil
zipWith3TC (TCCons k0 v t0) (TCCons k1 f1v t1) (TCCons k2 f2v t2) f =
case f k0 v k1 f1v k2 f2v of
(v', Dict) ->
TCCons k0 v' (zipWith3TC @kt @c0 @c1 @c2 @cr @f1 @f2 @r t0 t1 t2 f)
type DictOf c = TyCon1 Dict .@#@$$$ c
withTCDict
:: forall kt c0 c (kk :: [kt]) vv r
. TCTab c0 kk vv
-> TTab kk (Fmap (DictOf c) vv)
-> (ConstrainList (Fmap c vv) => r)
-> r
withTCDict TCNil TCNil f = f
withTCDict (TCCons _ _ tv) (TCCons _ Dict tc) f = withTCDict @_ @_ @c tv tc f
toTCDict
:: forall kt c0 c (kk :: [kt]) vv
. ConstrainList (Fmap c vv)
=> TCTab c0 kk vv
-> TTab kk (Fmap (DictOf c) vv)
toTCDict TCNil = TCNil
toTCDict (TCCons k _ xs) = TCCons k Dict (toTCDict @_ @_ @c xs)
weakenTC
:: forall kt c0 c1 (kk :: [kt]) vv
. ConstrainList (ZipWith (Class2Sym2 c1 c0) kk vv)
=> TCTab c0 kk vv
-> TCTab c1 kk vv
weakenTC TCNil = TCNil
weakenTC (TCCons (k :: Sing k) (v :: v) tab) =
case cls @(c1 @@ k @@ v) @(c0 @@ k @@ v) of
Sub Dict -> TCCons k v (weakenTC tab)
strengthenTC
:: forall kt c0 c1 (kk :: [kt]) vv
. ConstrainList (ZipWith c1 kk vv)
=> TCTab c0 kk vv
-> TCTab (AndC2 c0 c1) kk vv
strengthenTC TCNil = TCNil
strengthenTC (TCCons k v xs) = TCCons k v (strengthenTC @_ @_ @c1 xs)
strengthenTC0
:: forall kt c1 (kk :: [kt]) vv
. ConstrainList (ZipWith c1 kk vv)
=> TTab kk vv
-> TCTab c1 kk vv
strengthenTC0 TCNil = TCNil
strengthenTC0 (TCCons k v xs) = TCCons k v (strengthenTC0 @_ @c1 xs)