Safe Haskell	None
Language	Haskell2010

Language.Symantic.Typing.Variable

Contents

Type Var
- Comparison
Type EVar
- Type IndexVar
Class LenVars
Class AllocVars
Type NameVar
Class VarOccursIn
Type family VarsOf
Type Vars
- Type EVars
Type UsedVars
- Class UsedVarsOf
Type UnProxy

Synopsis

Documentation

data a :~~: b where Source #

Heterogeneous propositional equality: like (:~:) but prove also that the kinds are equal.

Constructors

HRefl :: a :~~: a

Type `Var`

data Var src vs v where Source #

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 k (Var k src) Source #
Methods allocVarsL :: Len Type len -> a vs x -> a ((Type ++ len) vs) x Source # allocVarsR :: Len Type len -> a vs x -> a ((Type ++ vs) len) x Source #
SourceInj (EVar src vs) src => KindOf kt (Var kt src vs) Source #
Methods kindOf :: a t -> Kind (SourceOf (a t)) (Var kt src vs) Source #
Show (Var kv src tys v) Source #
Methods showsPrec :: Int -> Var kv src tys v -> ShowS # show :: Var kv src tys v -> String # showList :: [Var kv src tys v] -> ShowS #
LenVars (Var kv src vs v) Source #
Methods lenVars :: Var kv src vs v -> Len Type (VarsOf (Var kv src vs v)) Source #
type SourceOf (Var kv src vs t) Source #
type SourceOf (Var kv src vs t) = src
type VarsOf (Var kv src vs v) Source #
type VarsOf (Var kv src vs v) = vs

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

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

Return the Kind of given Var.

Comparison

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

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

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

Type `EVar`

data EVar src vs Source #

Existential Var.

Constructors

EVar (Var src vs v)

Type `IndexVar`

type IndexVar = Int Source #

Index of a Var.

indexVar :: Var src vs v -> Int Source #

Class `LenVars`

class LenVars a where Source #

Return the Len of the Var context.

Minimal complete definition

lenVars

Methods

lenVars :: a -> Len (VarsOf a) Source #

Instances

LenVars (Vars src vs) Source #
Methods lenVars :: Vars src vs -> Len Type (VarsOf (Vars src vs)) Source #
LenVars (UsedVars src vs vs') Source #
Methods lenVars :: UsedVars src vs vs' -> Len Type (VarsOf (UsedVars src vs vs')) Source #
LenVars (Var kv src vs v) Source #
Methods lenVars :: Var kv src vs v -> Len Type (VarsOf (Var kv src vs v)) Source #
LenVars (Type kt src vs t) Source #
Methods lenVars :: Type kt src vs t -> Len Type (VarsOf (Type kt src vs t)) Source #
LenVars (Term src ss ts vs t) Source #
Methods lenVars :: Term src ss ts vs t -> Len Type (VarsOf (Term src ss ts vs t)) Source #

Class `AllocVars`

class AllocVars a where Source #

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

Minimal complete definition

allocVarsL, allocVarsR

Methods

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

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

Instances

AllocVars k (Var k src) Source #
Methods allocVarsL :: Len Type len -> a vs x -> a ((Type ++ len) vs) x Source # allocVarsR :: Len Type len -> a vs x -> a ((Type ++ vs) len) x Source #
AllocVars k (Type k src) Source #
Methods allocVarsL :: Len Type len -> a vs x -> a ((Type ++ len) vs) x Source # allocVarsR :: Len Type len -> a vs x -> a ((Type ++ vs) len) x Source #
AllocVars Type (Term src ss ts) Source #
Methods allocVarsL :: Len Type len -> a vs x -> a ((Type ++ len) vs) x Source # allocVarsR :: Len Type len -> a vs x -> a ((Type ++ vs) len) x Source #

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) Source #

Type `NameVar`

newtype NameVar Source #

Constructors

NameVar Text

Instances

Eq NameVar Source #
Methods (==) :: NameVar -> NameVar -> Bool # (/=) :: NameVar -> NameVar -> Bool #
Ord NameVar Source #
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 Source #
Methods showsPrec :: Int -> NameVar -> ShowS # show :: NameVar -> String # showList :: [NameVar] -> ShowS #
IsString NameVar Source #
Methods fromString :: String -> NameVar #

Class `VarOccursIn`

class VarOccursIn a where Source #

Test whether a given Var occurs within something.

Minimal complete definition

varOccursIn

Methods

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

Instances

VarOccursIn (Types src vs ts) Source #
Methods varOccursIn :: Var kv src (VarsOf (Types src vs ts)) v -> Types src vs ts -> Bool Source #
VarOccursIn (Type kt src vs t) Source #
Methods varOccursIn :: Var kv src (VarsOf (Type kt src vs t)) v -> Type kt src vs t -> Bool Source #

Type family `VarsOf`

type family VarsOf a :: [Type] Source #

Return the Var context of something.

Instances

type VarsOf (Vars src vs) Source #
type VarsOf (Vars src vs) = vs
type VarsOf (TypeT src vs) Source #
type VarsOf (TypeT src vs) = vs
type VarsOf (UsedVars src vs vs') Source #
type VarsOf (UsedVars src vs vs') = vs'
type VarsOf (Types src vs ts) Source #
type VarsOf (Types src vs ts) = vs
type VarsOf (TypeK src vs ki) Source #
type VarsOf (TypeK src vs ki) = vs
type VarsOf (Var kv src vs v) Source #
type VarsOf (Var kv src vs v) = vs
type VarsOf (Type kt src vs t) Source #
type VarsOf (Type kt src vs t) = vs
type VarsOf (Term src ss ts vs t) Source #
type VarsOf (Term src ss ts vs t) = vs

Type `Vars`

data Vars src vs where Source #

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) Source #
Methods lenVars :: Vars src vs -> Len Type (VarsOf (Vars src vs)) Source #
type VarsOf (Vars src vs) Source #
type VarsOf (Vars src vs) = vs

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

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

Type `EVars`

data EVars src Source #

Existential Vars.

Constructors

EVars (Vars src vs)

Type `UsedVars`

data UsedVars src vs vs' where Source #

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') Source #
Methods lenVars :: UsedVars src vs vs' -> Len Type (VarsOf (UsedVars src vs vs')) Source #
type VarsOf (UsedVars src vs vs') Source #
type VarsOf (UsedVars src vs vs') = vs'

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

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

Class `UsedVarsOf`

class UsedVarsOf a where Source #

Minimal complete definition

usedVarsOf

Methods

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

Instances

UsedVarsOf (Types src vs ts) Source #
Methods usedVarsOf :: UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs -> Types src vs ts -> (forall vs'. UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs' -> ret) -> ret Source #
UsedVarsOf (Type kt src vs t) Source #
Methods usedVarsOf :: UsedVars (SourceOf (Type kt src vs t)) (VarsOf (Type kt src vs t)) vs -> Type kt src vs t -> (forall vs'. UsedVars (SourceOf (Type kt src vs t)) (VarsOf (Type kt src vs t)) vs' -> ret) -> ret Source #

Type `UnProxy`

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

Equations

UnProxy (Proxy x) = x

Documentation

Type Var

Comparison

Type EVar

Type IndexVar

Class LenVars

Class AllocVars

Type NameVar

Class VarOccursIn

Type family VarsOf

Type Vars

Type EVars

Type UsedVars

Class UsedVarsOf

Type UnProxy

Type `Var`

Type `EVar`

Type `IndexVar`

Class `LenVars`

Class `AllocVars`

Type `NameVar`

Class `VarOccursIn`

Type family `VarsOf`

Type `Vars`

Type `EVars`

Type `UsedVars`

Class `UsedVarsOf`

Type `UnProxy`