on be54907 help sign in
rel8/src/Rel8/Schema/Context/Abstract.hs
80 lines 1.7 kB history raw
1{-# language DataKinds #-}
2{-# language GADTs #-}
3{-# language LambdaCase #-}
4{-# language StandaloneKindSignatures #-}
5{-# language TypeFamilies #-}
6{-# language TypeOperators #-}
8module Rel8.Schema.Context.Abstract
9 ( Abstract, virtual
10 , Virtual(..), virtualOrResult, exclusivity
11 )
12where
14-- base
15import Data.Kind ( Constraint, Type )
16import Data.Type.Equality ( (:~:)( Refl) )
17import Prelude
19-- rel8
20import Rel8.Aggregate ( Aggregate )
21import Rel8.Expr ( Expr )
22import Rel8.Kind.Context ( SContext(..) )
23import qualified Rel8.Schema.Kind as K
24import Rel8.Schema.Name ( Name )
25import Rel8.Schema.Reify ( Reify )
26import Rel8.Schema.Result ( Result, NotResult( NotResult ) )
29type Abstract :: K.Context -> Constraint
30type family Abstract context where
31 Abstract (Reify context) = IsVirtual context
32 Abstract _ = ()
35type IsVirtual :: K.Context -> Constraint
36class IsVirtual context where
37 virtual :: Virtual context
40instance IsVirtual Aggregate where
41 virtual = VAggregate
44instance IsVirtual Expr where
45 virtual = VExpr
48instance IsVirtual Name where
49 virtual = VName
52instance IsVirtual (Reify context) where
53 virtual = VReify
56type Virtual :: K.Context -> Type
57data Virtual context where
58 VAggregate :: Virtual Aggregate
59 VExpr :: Virtual Expr
60 VName :: Virtual Name
61 VReify :: Virtual (Reify context)
64virtualOrResult :: ()
65 => SContext context
66 -> Either (context :~: Result) (Virtual context)
67virtualOrResult = \case
68 SAggregate -> Right VAggregate
69 SExpr -> Right VExpr
70 SName -> Right VName
71 SResult -> Left Refl
72 SReify _ -> Right VReify
75exclusivity :: Virtual context -> NotResult context
76exclusivity = \case
77 VAggregate -> NotResult
78 VExpr -> NotResult
79 VName -> NotResult
80 VReify -> NotResult