Copyright	(c) Juan García Garland 2018
License	LGPL
Maintainer	jpgarcia@fing.edu.uy
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

Language.Grammars.AspectAG.TPrelude

Description

Synopsis

data Label l = Label
sndLabel :: Label '(a, b) -> Label b
getProxy :: a -> Proxy a
getLabel :: a -> Label a
proxyFrom :: t a -> Proxy a
type family If (cond :: Bool) (thn :: k) (els :: k) :: k where ...
type family Or (l :: Bool) (r :: Bool) :: Bool where ...
type family And (l :: Bool) (r :: Bool) :: Bool where ...
type family Not (l :: Bool) :: Bool where ...
type family LabelSetF (r :: [(k, k')]) :: Bool where ...
type LabelSet r = LabelSetF r ~ True
type family And3 (a1 :: Bool) (a2 :: Bool) (a3 :: Bool) where ...
type family HMemberT (e :: k) (l :: [k]) :: Bool where ...
type family HasLabelT (l :: k) (lst :: [(k, Type)]) :: Bool where ...
class HEq (x :: k) (y :: k) (b :: Bool) | x y -> b
type HEqK (x :: k1) (y :: k2) (b :: Bool) = HEq (Proxy x) (Proxy y) b
type family HEqKF (a :: k) (b :: k) :: Bool
type family (a :: k1) === (b :: k2) where ...
type family TPair (a :: k) b where ...
type family LabelsOf (r :: [(k, k')]) :: [k] where ...
type family HasLabel (l :: k) (r :: [(k, k')]) :: Bool where ...
type family Equal (a :: k) (b :: k') :: Bool where ...

Documentation

data Label l Source #

Constructors

Label

sndLabel :: Label '(a, b) -> Label b Source #

getProxy :: a -> Proxy a Source #

getLabel :: a -> Label a Source #

proxyFrom :: t a -> Proxy a Source #

type family If (cond :: Bool) (thn :: k) (els :: k) :: k where ... Source #

If construction, purely computed at type level

Equations

If True thn els = thn
If False thn els = els

type family Or (l :: Bool) (r :: Bool) :: Bool where ... Source #

Or, purely computed at type level

Equations

Or False b = b
Or True b = True

type family And (l :: Bool) (r :: Bool) :: Bool where ... Source #

And, purely computed at type level

Equations

And False b = False
And True b = b

type family Not (l :: Bool) :: Bool where ... Source #

Not, purely computed at type level

Equations

Not False = True
Not True = False

type family LabelSetF (r :: [(k, k')]) :: Bool where ... Source #

LabelSet is a predicate over lists of pairs. We assume the list represent a (partial) mapping from k1 to k2. k1 is a label, k2 possibly a value. The first member of each pair must be unique, this is a predicate of well formedness class LabelSet (l :: [(k1,k2)])

Equations

LabelSetF '[] = True
LabelSetF '['(l, v)] = True
LabelSetF ('(l, v) ': ('(l', v') ': r)) = And3 (Not (l == l')) (LabelSetF ('(l, v) ': r)) (LabelSetF ('(l', v') ': r))

type LabelSet r = LabelSetF r ~ True Source #

type family And3 (a1 :: Bool) (a2 :: Bool) (a3 :: Bool) where ... Source #

Equations

And3 True True True = True
And3 _ _ _ = False

type family HMemberT (e :: k) (l :: [k]) :: Bool where ... Source #

Predicate of membership, for lists at type level

Equations

HMemberT k '[] = False
HMemberT k (k' ': l) = If (k == k') True (HMemberT k l)

type family HasLabelT (l :: k) (lst :: [(k, Type)]) :: Bool where ... Source #

Predicate of membership, for labels at type level

Equations

HasLabelT l '[] = False
HasLabelT l ('(k, v) ': tail) = If (l == k) True (HasLabelT l tail)

class HEq (x :: k) (y :: k) (b :: Bool) | x y -> b Source #

This is used for type Equality

Instances

(Proxy x == Proxy y) ~ b => HEq (x :: k) (y :: k) b Source #
Instance details Defined in Language.Grammars.AspectAG.TPrelude

type HEqK (x :: k1) (y :: k2) (b :: Bool) = HEq (Proxy x) (Proxy y) b Source #

type family HEqKF (a :: k) (b :: k) :: Bool Source #

Instances

type HEqKF (a :: k) (b :: k) Source #
Instance details Defined in Language.Grammars.AspectAG.TPrelude type HEqKF (a :: k) (b :: k) = a == b

type family (a :: k1) === (b :: k2) where ... Source #

heterogeneous equality at type level

Equations

a === b = Proxy a == Proxy b

type family TPair (a :: k) b where ... Source #

Equations

TPair a b = '(a, b)

type family LabelsOf (r :: [(k, k')]) :: [k] where ... Source #

Equations

LabelsOf '[] = '[]
LabelsOf ('(k, ks) ': ls) = k ': LabelsOf ls

type family HasLabel (l :: k) (r :: [(k, k')]) :: Bool where ... Source #

Equations

HasLabel l '[] = False
HasLabel l ('(l', v) ': r) = Or (l == l') (HasLabel l r)

type family Equal (a :: k) (b :: k') :: Bool where ... Source #

Equations

Equal a a = True
Equal a b = False