ermine-0.6: Ermine

Copyright(c) Edward Kmett 2011-2012
LicenseBSD3
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Ermine.Unification.Meta

Contents

Description

Meta variables

Synopsis

Meta variables

data Meta s f a Source

A meta variable for skolemization and unification

Constructors

Meta a Hint !Int !(STRef s (Maybe (f (Meta s f a)))) !(STRef s Depth) !(STRef s Rank) 

Instances

Eq (Meta s f a) 
Ord (Meta s f a) 
Show a => Show (Meta s f a) 

metaId :: forall s f a. Lens' (Meta s f a) Int Source

metaValue :: forall s f a. Lens' (Meta s f a) a Source

metaRef :: forall s f a f. Lens (Meta s f a) (Meta s f a) (STRef s (Maybe (f (Meta s f a)))) (STRef s (Maybe (f (Meta s f a)))) Source

metaHint :: forall s f a. Lens' (Meta s f a) Hint Source

Meta Types

type MetaT s = Meta s (Type (MetaK s)) (KindM s) Source

A type meta-variable

type TypeM s = Type (MetaK s) (MetaT s) Source

A type filled with meta-variables

Meta Kinds

type MetaK s = Meta s Kind Bool Source

A kind meta-variable

type KindM s = Kind (MetaK s) Source

A kind filled with meta-variables

λ-Depth

type Depth = Int Source

Kuan and MacQueen's notion of λ-ranking.

metaDepth :: forall s f a. Lens' (Meta s f a) (STRef s Depth) Source

depthInf :: Depth Source

This plays the role of infinity.

Union-By-Rank

type Rank = Word Source

Rank for union-by-rank viewing meta-variables as disjoint set forests

metaRank :: forall s f a. Lens' (Meta s f a) (STRef s Rank) Source

bumpRank :: STRef s Rank -> ST s () Source

Working with Meta

newMeta :: MonadMeta s m => a -> Hint -> m (Meta s f a) Source

Construct a new meta variable

newShallowMeta :: MonadMeta s m => Depth -> a -> Hint -> m (Meta s f a) Source

Construct a new meta variable at a given depth

readMeta :: MonadMeta s m => Meta s f a -> m (Maybe (f (Meta s f a))) Source

Read a meta variable

writeMeta :: MonadMeta s m => Meta s f a -> f (Meta s f a) -> m () Source

Write to a meta variable

Pruning

semiprune :: (Variable f, Monad f, MonadMeta s m) => f (Meta s f a) -> m (f (Meta s f a)) Source

Path-compression

zonk :: (MonadMeta s m, MonadWriter Any m, Traversable f, Monad f) => f (Meta s f a) -> m (f (Meta s f a)) Source

Expand meta variables recursively

zonk_ :: (MonadMeta s m, Traversable f, Monad f) => f (Meta s f a) -> m (f (Meta s f a)) Source

zonkWith :: (MonadMeta s m, MonadWriter Any m, Traversable f, Monad f) => f (Meta s f a) -> (Meta s f a -> m ()) -> m (f (Meta s f a)) Source

zonkScope :: (MonadMeta s m, MonadWriter Any m, Traversable f, Monad f) => Scope b f (Meta s f a) -> m (Scope b f (Meta s f a)) Source

zonkScope_ :: (MonadMeta s m, Traversable f, Monad f) => Scope b f (Meta s f a) -> m (Scope b f (Meta s f a)) Source

hasSkolems :: (Traversable f, Monad f, MonadMeta s m) => LensLike' m ts (f (Meta s f a)) -> [Meta s f a] -> ts -> m ts Source

Checks if any of the listed skolems exists in the types given in the traversal.

checkSkolems :: MonadMeta s m => Maybe Depth -> LensLike' m ts (TypeM s) -> [MetaT s] -> ts -> m ts Source

Check for escaped Skolem variables in any container full of types.

Dies due to an escaped Skolem or returns the container with all of its types fully zonked.

checkEscapes :: MonadMeta s m => Depth -> [Meta s f a] -> m () Source

Checks if any of the skolems in the list escapes into the context defined by the given depth.

checkDistinct :: (Traversable f, Monad f, Variable f, MonadMeta s m) => [Meta s f a] -> m [Meta s f a] Source

MetaEnv

data MetaEnv s Source

Instances

class HasMetaEnv t s | t -> s where Source

Minimal complete definition

metaEnv

Methods

metaEnv :: Lens' t (MetaEnv s) Source

metaFresh :: Lens' t (STRef s Int) Source

metaMemory :: Lens' t (STRef s (IntMap (TypeM s))) Source

metaRendering :: Lens' t Rendering Source

Instances

class (Applicative m, MonadST m, s ~ World m) => MonadMeta s m | m -> s where Source

Minimal complete definition

localMeta

Methods

askMeta :: m (MetaEnv s) Source

localMeta :: (MetaEnv s -> MetaEnv s) -> m a -> m a Source

Instances

MonadMeta s m => MonadMeta s (MaybeT m) 
MonadMeta s (M s) 
MonadMeta s m => MonadMeta s (SharingT m) 
MonadMeta s m => MonadMeta s (StateT t m) 
MonadMeta s m => MonadMeta s (StateT t m) 
MonadMeta s (CM cc s) 

viewMeta :: MonadMeta s m => Getting a (MetaEnv s) a -> m a Source

The unification monad

data M s a Source

The unification monad provides a fresh variable supply and tracks a current Rendering to blame for any unification errors.

Instances

MonadMeta s (M s) 
Monad (M s) 
Functor (M s) 
Applicative (M s) 
MonadST (M s) 
Monoid m => Monoid (M s m) 
type World (M s) = s 

runM :: Rendering -> (forall s. M s a) -> Either Diagnostic a Source

Evaluate an expression in the M Monad with a fresh variable supply.

runM_ :: Rendering -> (forall s. M s a) -> a Source

Evaluate an expression in the M Monad with a fresh variable supply, throwing any errors returned.

ioM :: MonadIO m => Rendering -> (forall s. M s a) -> m a Source

Evaluate an expression in the M Monad with a fresh variable supply, throwing any errors returned.

throwM :: MonadST m => Diagnostic -> m a Source

Throw a Diagnostic error.

fresh :: MonadMeta s m => m Int Source

Generate a fresh variable

remember :: MonadMeta s m => Int -> TypeM s -> m () Source