DDC.Core.Flow.Transform.Rates.SizeInference

Performing size inference on a program in Combinator Normal Form

Documentation

data Type v

tau ::=

Constructors

TVar (K v)

k

TCross (Type v) (Type v)

tau * tau

Instances

Eq v => Eq (Type v)

Ord v => Ord (Type v)

Show v => Show (Type v)

Pretty v => Pretty (Maybe (Type v))

Pretty v => Pretty (Type v)

data K v

Given some variable type, append a number of primes onto it. We want to be able to distinguish between the raw variable types and unification, existential Klock (rate) variables. We generate constraints so that raw variables will appear on the left of equalities, and Ks may appear on the right.

Constructors

KV v

K' (K v)

Instances

Eq v => Eq (K v)

Ord v => Ord (K v)

Show v => Show (K v)

Pretty v => Pretty (K v)

type Env v = [Scope v]

Gamma ::= • | Gamma, Gamma...

data Scope v

Gamma ::= ...

Constructors

EVar v (Type v)

v : k

EUnify (K v)

k

ERigid (K v)

exists k

Instances

Show v => Show (Scope v)

Pretty v => Pretty (Scope v)

data Scheme v

sigma ::= forall k... exists k... (x : t)... -> (x : t)... Note that these are all raw variable types. There is no point mentioning unification variables in this solved form.

Constructors

Scheme

Fields

_forall :: [K v]

_exists :: [K v]

_from :: [(v, Type v)]

_to :: [(v, Type v)]

Instances

Show v => Show (Scheme v)

Pretty v => Pretty (Scheme v)

generate :: Ord a => Program s a -> Maybe (Env a, Scheme a)

program :_s sigma

lookupV :: Eq v => Env v -> v -> Maybe (Type v)

Search for first (should be only) mention of k in environment, along with its index

iter :: (Eq a, Eq s) => Program s a -> Env a -> CName s a -> Maybe (Type a)

Find iteration size of given combinator

parents :: (Eq a, Eq s) => Program s a -> Env a -> CName s a -> CName s a -> Maybe (CName s a, CName s a)

Find pair of parent transducers with same iteration size

trans :: (Eq a, Eq s) => Program s a -> CName s a -> Maybe (CName s a)

Find a bindings' transducer. Only array bindings can have transducers.