DDC.Source.Tetra.Transform.Expand

Look at type signatures and add quantifiers to bind any free type variables. Also add holes for missing type arguments.

Given

   mapS (f : a -> S e b) (xx : List a) : S e (List b)
    = box case xx of
       Nil        -> Nil
       Cons x xs  -> Cons (run f x) (run mapS f xs)

We get:

   mapS [a e b : ?] (f : a -> S e b) (xx : List a) : S e (List b)
    = /(a e b : ?). box case xx of
       Nil        -> Nil
       Cons x xs  -> Cons (run f x) (run mapS [?] [?] [?] f xs)

Documentation

data Config l

Expander configuration.

Constructors

Config

Fields

configMakeTypeHole :: Kind (GName l) -> Type (GName l)

Make a type hole of the given kind.

configDefault :: (GName l ~ Name) => Config l

Default expander configuration.

class ExpandLanguage l => Expand c l where

Methods

expand :: Ord (GName l) => Config l -> KindEnv (GName l) -> TypeEnv (GName l) -> c l -> c l

Add quantifiers to the types of binders. Also add holes for missing type arguments.

Instances

ExpandLanguage l => Expand GGuard l

ExpandLanguage l => Expand GGuardedExp l

ExpandLanguage l => Expand GAlt l

ExpandLanguage l => Expand GExp l

ExpandLanguage l => Expand Top l

ExpandLanguage l => Expand Module l