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)

Methods

(==) :: Type v -> Type v -> Bool

(/=) :: Type v -> Type v -> Bool

Ord v => Ord (Type v)

Methods

compare :: Type v -> Type v -> Ordering

(<) :: Type v -> Type v -> Bool

(<=) :: Type v -> Type v -> Bool

(>) :: Type v -> Type v -> Bool

(>=) :: Type v -> Type v -> Bool

max :: Type v -> Type v -> Type v

min :: Type v -> Type v -> Type v

Show v => Show (Type v)

Methods

showsPrec :: Int -> Type v -> ShowS

show :: Type v -> String

showList :: [Type v] -> ShowS

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

Associated Types

data PrettyMode (Maybe (Type v)) :: *

Methods

pprDefaultMode :: PrettyMode (Maybe (Type v))

ppr :: Maybe (Type v) -> Doc

pprPrec :: Int -> Maybe (Type v) -> Doc

pprModePrec :: PrettyMode (Maybe (Type v)) -> Int -> Maybe (Type v) -> Doc

Pretty v => Pretty (Type v)

Associated Types

data PrettyMode (Type v) :: *

Methods

pprDefaultMode :: PrettyMode (Type v)

ppr :: Type v -> Doc

pprPrec :: Int -> Type v -> Doc

pprModePrec :: PrettyMode (Type v) -> Int -> Type v -> Doc

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)

Methods

(==) :: K v -> K v -> Bool

(/=) :: K v -> K v -> Bool

Ord v => Ord (K v)

Methods

compare :: K v -> K v -> Ordering

(<) :: K v -> K v -> Bool

(<=) :: K v -> K v -> Bool

(>) :: K v -> K v -> Bool

(>=) :: K v -> K v -> Bool

max :: K v -> K v -> K v

min :: K v -> K v -> K v

Show v => Show (K v)

Methods

showsPrec :: Int -> K v -> ShowS

show :: K v -> String

showList :: [K v] -> ShowS

Pretty v => Pretty (K v)

Associated Types

data PrettyMode (K v) :: *

Methods

pprDefaultMode :: PrettyMode (K v)

ppr :: K v -> Doc

pprPrec :: Int -> K v -> Doc

pprModePrec :: PrettyMode (K v) -> Int -> K v -> Doc

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)

Methods

showsPrec :: Int -> Scope v -> ShowS

show :: Scope v -> String

showList :: [Scope v] -> ShowS

Pretty v => Pretty (Scope v)

Associated Types

data PrettyMode (Scope v) :: *

Methods

pprDefaultMode :: PrettyMode (Scope v)

ppr :: Scope v -> Doc

pprPrec :: Int -> Scope v -> Doc

pprModePrec :: PrettyMode (Scope v) -> Int -> Scope v -> Doc

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)

Methods

showsPrec :: Int -> Scheme v -> ShowS

show :: Scheme v -> String

showList :: [Scheme v] -> ShowS

Pretty v => Pretty (Scheme v)

Associated Types

data PrettyMode (Scheme v) :: *

Methods

pprDefaultMode :: PrettyMode (Scheme v)

ppr :: Scheme v -> Doc

pprPrec :: Int -> Scheme v -> Doc

pprModePrec :: PrettyMode (Scheme v) -> Int -> Scheme v -> Doc

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.