Tip.Scope

Contents

• Querying the scope
• The scope monad
• Adding things to the scope in the scope monad

Description

Synopsis

• scope :: (PrettyVar a, Ord a) => Theory a -> Scope a
• data Scope a = Scope {
  • inner :: Set a
  • types :: Map a (TypeInfo a)
  • locals :: Map a (Type a)
  • globals :: Map a (GlobalInfo a)
  }
• data TypeInfo a
  • = TyVarInfo
  • | DatatypeInfo (Datatype a)
  • | SortInfo (Sort a)
• data GlobalInfo a
  • = FunctionInfo (PolyType a)
  • | ConstructorInfo (Datatype a) (Constructor a)
  • | ProjectorInfo (Datatype a) (Constructor a) Int (Type a)
  • | DiscriminatorInfo (Datatype a) (Constructor a)
• globalType :: GlobalInfo a -> PolyType a
• isType :: Ord a => a -> Scope a -> Bool
• isTyVar :: Ord a => a -> Scope a -> Bool
• isSort :: Ord a => a -> Scope a -> Bool
• isLocal :: Ord a => a -> Scope a -> Bool
• isGlobal :: Ord a => a -> Scope a -> Bool
• lookupType :: Ord a => a -> Scope a -> Maybe (TypeInfo a)
• lookupLocal :: Ord a => a -> Scope a -> Maybe (Type a)
• lookupGlobal :: Ord a => a -> Scope a -> Maybe (GlobalInfo a)
• lookupDatatype :: Ord a => a -> Scope a -> Maybe (Datatype a)
• lookupFunction :: Ord a => a -> Scope a -> Maybe (PolyType a)
• lookupConstructor :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)
• lookupDiscriminator :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)
• lookupProjector :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a, Int, Type a)
• whichDatatype :: Ord a => a -> Scope a -> Datatype a
• whichLocal :: Ord a => a -> Scope a -> Type a
• whichGlobal :: Ord a => a -> Scope a -> GlobalInfo a
• whichFunction :: Ord a => a -> Scope a -> PolyType a
• whichConstructor :: Ord a => a -> Scope a -> (Datatype a, Constructor a)
• whichDiscriminator :: Ord a => a -> Scope a -> (Datatype a, Constructor a)
• whichProjector :: Ord a => a -> Scope a -> (Datatype a, Constructor a, Int, Type a)
• newtype ScopeT a m b = ScopeT {
  • unScopeT :: StateT (Scope a) (ErrorT Doc m) b
  }
• runScopeT :: Monad m => ScopeT a m b -> m (Either Doc b)
• checkScopeT :: Monad m => ScopeT a m b -> m b
• type ScopeM a = ScopeT a Identity
• runScope :: ScopeM a b -> Either Doc b
• checkScope :: ScopeM a b -> b
• emptyScope :: Scope a
• inContext :: Pretty a => a -> ScopeM b c -> ScopeM b c
• local :: Monad m => ScopeT a m b -> ScopeT a m b
• newScope :: Monad m => ScopeT a m b -> ScopeT a m b
• newName :: (PrettyVar a, Ord a, Monad m) => a -> ScopeT a m ()
• newTyVar :: (Monad m, Ord a, PrettyVar a) => a -> ScopeT a m ()
• newSort :: (Monad m, Ord a, PrettyVar a) => Sort a -> ScopeT a m ()
• newDatatype :: (Monad m, Ord a, PrettyVar a) => Datatype a -> ScopeT a m ()
• newConstructor :: (Monad m, Ord a, PrettyVar a) => Datatype a -> Constructor a -> ScopeT a m ()
• newFunction :: (Monad m, Ord a, PrettyVar a) => Signature a -> ScopeT a m ()
• newLocal :: (Monad m, Ord a, PrettyVar a) => Local a -> ScopeT a m ()
• withTheory :: (Monad m, Ord a, PrettyVar a) => Theory a -> ScopeT a m b -> ScopeT a m b

Documentation

Querying the scope

The scope monad

Adding things to the scope in the scope monad