symantic-6.3.0.20170807: Library for Typed Tagless-Final Higher-Order Composable DSL

Safe HaskellNone
LanguageHaskell2010

Language.Symantic.Typing.Variable

Contents

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

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