Language.Symantic.Typing.Variable

Type Var

data Var src (vs :: [Type]) (v :: kv) where

A type variable, indexed amongst a type-level list. v is wrapped within a Proxy to have a kind-heterogeneous list.

Constructors

VarZ :: Kind src kv -> Len (Proxy (v :: kv) ': vs) -> Var src (Proxy (v :: kv) ': vs) (v :: kv)

VarS :: Var src vs v -> Var src (not_v ': vs) v infixr 5

Instances

AllocVars (Var src :: [Type] -> k -> Type)

Defined in Language.Symantic.Typing.Variable

Methods

allocVarsL :: Len len -> Var src vs x -> Var src (len ++ vs) x

allocVarsR :: Len len -> Var src vs x -> Var src (vs ++ len) x

SourceInj (EVar src vs) src => KindOf (Var src vs :: kt -> Type)

Defined in Language.Symantic.Typing.Variable

Methods

kindOf :: Var src vs t -> Kind (SourceOf (Var src vs t)) kt0

Show (Var src tys v)

Defined in Language.Symantic.Typing.Variable

Methods

showsPrec :: Int -> Var src tys v -> ShowS

show :: Var src tys v -> String

showList :: [Var src tys v] -> ShowS

LenVars (Var src vs v)

Defined in Language.Symantic.Typing.Variable

Methods

lenVars :: Var src vs v -> Len (VarsOf (Var src vs v))

type SourceOf (Var src vs t)

Defined in Language.Symantic.Typing.Variable

type SourceOf (Var src vs t) = src

type VarsOf (Var src vs v)

Defined in Language.Symantic.Typing.Variable

type VarsOf (Var src vs v) = vs

varZ :: forall src vs kv (v :: kv). Source src => LenInj vs => KindInj kv => Var src (Proxy v ': vs) v

kindOfVar :: Var src vs (v :: kv) -> Kind src kv

Return the Kind of given Var.

Comparison

eqVar :: Var xs vs x -> Var ys vs y -> Maybe (x :~: y)

eqVarKi :: Var xs vs x -> Var ys vs y -> Maybe ((x :: kx) :~~: (y :: ky))

ordVarKi :: Var xs vs x -> Var ys vs y -> Ordering

Type EVar

data EVar src vs

Existential Var.

Constructors

EVar (Var src vs v)

Type IndexVar

type IndexVar = Int

Index of a Var.

indexVar :: Var src vs v -> Int

Class LenVars

class LenVars a where

Return the Len of the Var context.

Methods

lenVars :: a -> Len (VarsOf a)

Instances

LenVars (Vars src vs)

Defined in Language.Symantic.Typing.Variable

Methods

lenVars :: Vars src vs -> Len (VarsOf (Vars src vs))

LenVars (UsedVars src vs vs')

Defined in Language.Symantic.Typing.Variable

Methods

lenVars :: UsedVars src vs vs' -> Len (VarsOf (UsedVars src vs vs'))

LenVars (Var src vs v)

Defined in Language.Symantic.Typing.Variable

Methods

lenVars :: Var src vs v -> Len (VarsOf (Var src vs v))

LenVars (Type src vs t)

Defined in Language.Symantic.Typing.Type

Methods

lenVars :: Type src vs t -> Len (VarsOf (Type src vs t))

LenVars (Term src ss ts vs t)

Defined in Language.Symantic.Compiling.Term

Methods

lenVars :: Term src ss ts vs t -> Len (VarsOf (Term src ss ts vs t))

Class AllocVars

class AllocVars (a :: [Type] -> k -> Type) where

Allocate Vars in a Var context, either to the left or to the right.

Methods

allocVarsL :: Len len -> a vs x -> a (len ++ vs) x

allocVarsR :: Len len -> a vs x -> a (vs ++ len) x

Instances

AllocVars (Var src :: [Type] -> k -> Type)

Defined in Language.Symantic.Typing.Variable

Methods

allocVarsL :: Len len -> Var src vs x -> Var src (len ++ vs) x

allocVarsR :: Len len -> Var src vs x -> Var src (vs ++ len) x

AllocVars (Type src :: [Type] -> k -> Type)

Defined in Language.Symantic.Typing.Type

Methods

allocVarsL :: Len len -> Type src vs x -> Type src (len ++ vs) x

allocVarsR :: Len len -> Type src vs x -> Type src (vs ++ len) x

AllocVars (Term src ss ts :: [Type] -> Type -> Type)

Defined in Language.Symantic.Compiling.Term

Methods

allocVarsL :: Len len -> Term src ss ts vs x -> Term src ss ts (len ++ vs) x

allocVarsR :: Len len -> Term src ss ts vs x -> Term src ss ts (vs ++ len) x

appendVars :: AllocVars a => AllocVars b => LenVars (a vs_x x) => LenVars (b vs_y y) => VarsOf (a vs_x x) ~ vs_x => VarsOf (b vs_y y) ~ vs_y => a vs_x (x :: kx) -> b vs_y (y :: ky) -> (a (vs_x ++ vs_y) x, b (vs_x ++ vs_y) y)

Type NameVar

newtype NameVar

Constructors

NameVar Text

Instances

Eq NameVar

Defined in Language.Symantic.Typing.Variable

Methods

(==) :: NameVar -> NameVar -> Bool

(/=) :: NameVar -> NameVar -> Bool

Ord NameVar

Defined in Language.Symantic.Typing.Variable

Methods

compare :: NameVar -> NameVar -> Ordering

(<) :: NameVar -> NameVar -> Bool

(<=) :: NameVar -> NameVar -> Bool

(>) :: NameVar -> NameVar -> Bool

(>=) :: NameVar -> NameVar -> Bool

max :: NameVar -> NameVar -> NameVar

min :: NameVar -> NameVar -> NameVar

Show NameVar

Defined in Language.Symantic.Typing.Variable

Methods

showsPrec :: Int -> NameVar -> ShowS

show :: NameVar -> String

showList :: [NameVar] -> ShowS

IsString NameVar

Defined in Language.Symantic.Typing.Variable

Methods

fromString :: String -> NameVar

Class VarOccursIn

class VarOccursIn a where

Test whether a given Var occurs within something.

Methods

varOccursIn :: Var src (VarsOf a) v -> a -> Bool

Instances

VarOccursIn (Types src vs ts)

Defined in Language.Symantic.Typing.Type

Methods

varOccursIn :: Var src0 (VarsOf (Types src vs ts)) v -> Types src vs ts -> Bool

VarOccursIn (Type src vs t)

Defined in Language.Symantic.Typing.Type

Methods

varOccursIn :: Var src0 (VarsOf (Type src vs t)) v -> Type src vs t -> Bool

Type family VarsOf

type family VarsOf a :: [Type]

Return the Var context of something.

Instances

type VarsOf (Vars src vs)

Defined in Language.Symantic.Typing.Variable

type VarsOf (Vars src vs) = vs

type VarsOf (TypeT src vs)

Defined in Language.Symantic.Typing.Type

type VarsOf (TypeT src vs) = vs

type VarsOf (UsedVars src vs vs')

Defined in Language.Symantic.Typing.Variable

type VarsOf (UsedVars src vs vs') = vs'

type VarsOf (Types src vs ts)

Defined in Language.Symantic.Typing.Type

type VarsOf (Types src vs ts) = vs

type VarsOf (TypeK src vs ki)

Defined in Language.Symantic.Typing.Type

type VarsOf (TypeK src vs ki) = vs

type VarsOf (Var src vs v)

Defined in Language.Symantic.Typing.Variable

type VarsOf (Var src vs v) = vs

type VarsOf (Type src vs t)

Defined in Language.Symantic.Typing.Type

type VarsOf (Type src vs t) = vs

type VarsOf (Term src ss ts vs t)

Defined in Language.Symantic.Compiling.Term

type VarsOf (Term src ss ts vs t) = vs

Type Vars

data Vars src vs where

Growable list of Vars.

Constructors

VarsZ :: Vars src '[]

VarsS :: NameVar -> Kind src kv -> Vars src vs -> Vars src (Proxy (v :: kv) ': vs)

Instances

LenVars (Vars src vs)

Defined in Language.Symantic.Typing.Variable

Methods

lenVars :: Vars src vs -> Len (VarsOf (Vars src vs))

type VarsOf (Vars src vs)

Defined in Language.Symantic.Typing.Variable

type VarsOf (Vars src vs) = vs

lookupVars :: NameVar -> Vars src vs -> Maybe (EVar src vs)

insertVars :: NameVar -> Kind src k -> Vars src vs -> (forall vs'. Vars src vs' -> ret) -> ret

Type EVars

data EVars src

Existential Vars.

Constructors

EVars (Vars src vs)

Type UsedVars

data UsedVars src vs vs' where

List of Vars, used to change the context of a Var when removing unused Vars.

Constructors

UsedVarsZ :: UsedVars src vs '[]

UsedVarsS :: Var src vs (v :: k) -> UsedVars src vs vs' -> UsedVars src vs (Proxy v ': vs')

Instances

LenVars (UsedVars src vs vs')

Defined in Language.Symantic.Typing.Variable

Methods

lenVars :: UsedVars src vs vs' -> Len (VarsOf (UsedVars src vs vs'))

type VarsOf (UsedVars src vs vs')

Defined in Language.Symantic.Typing.Variable

type VarsOf (UsedVars src vs vs') = vs'

lookupUsedVars :: Var src vs v -> UsedVars src vs vs' -> Maybe (Var src vs' v)

insertUsedVars :: Var src vs v -> UsedVars src vs vs' -> Maybe (UsedVars src vs (Proxy v ': vs'))

Class UsedVarsOf

class UsedVarsOf a where

Methods

usedVarsOf :: UsedVars (SourceOf a) (VarsOf a) vs -> a -> (forall vs'. UsedVars (SourceOf a) (VarsOf a) vs' -> ret) -> ret

Instances

UsedVarsOf (Types src vs ts)

Defined in Language.Symantic.Typing.Type

Methods

usedVarsOf :: UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs0 -> Types src vs ts -> (forall (vs' :: [Type]). UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs' -> ret) -> ret

UsedVarsOf (Type src vs t)

Defined in Language.Symantic.Typing.Type

Methods

usedVarsOf :: UsedVars (SourceOf (Type src vs t)) (VarsOf (Type src vs t)) vs0 -> Type src vs t -> (forall (vs' :: [Type0]). UsedVars (SourceOf (Type src vs t)) (VarsOf (Type src vs t)) vs' -> ret) -> ret

Type UnProxy

type family UnProxy (x :: Type) :: k where ...

Equations

UnProxy (Proxy x) = x