Mikan
Safe HaskellNone
LanguageHaskell2010

Mikan.Syntax.Internal.Telescope

Contents

Synopsis

Telescopes

data Tele a Source #

Sequence of types. An argument of the first type is bound in later types and so on.

Constructors

EmptyTel 

Bundled Patterns

pattern ExtendTel :: a -> Abs (Tele a) -> Tele a 

Instances

Instances details
GetDefs Telescope Source # 
Instance details

Defined in Mikan.Syntax.Internal.Defs

Methods

getDefs :: (Monoid m, ExpandCase LiftedRep m) => (MetaId -> Maybe Term) -> (QName -> m) -> Telescope -> m Source #

Reify Telescope Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

Methods

reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source #

reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope) Source #

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Mikan.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope Source #

AddContext Telescope Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Telescope -> m a -> m a Source #

PrettyTCM Telescope Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Telescope -> m Doc Source #

Reduce Telescope Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope Source #

reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #

TeleNoAbs Telescope Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term Source #

Abstract Telescope Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

abstract :: Telescope -> Telescope -> Telescope Source #

Functor Tele Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

fmap :: (a -> b) -> Tele a -> Tele b #

(<$) :: a -> Tele b -> Tele a #

Foldable Tele Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

fold :: Monoid m => Tele m -> m #

foldMap :: Monoid m => (a -> m) -> Tele a -> m #

foldMap' :: Monoid m => (a -> m) -> Tele a -> m #

foldr :: (a -> b -> b) -> b -> Tele a -> b #

foldr' :: (a -> b -> b) -> b -> Tele a -> b #

foldl :: (b -> a -> b) -> b -> Tele a -> b #

foldl' :: (b -> a -> b) -> b -> Tele a -> b #

foldr1 :: (a -> a -> a) -> Tele a -> a #

foldl1 :: (a -> a -> a) -> Tele a -> a #

toList :: Tele a -> [a] #

null :: Tele a -> Bool #

length :: Tele a -> Int #

elem :: Eq a => a -> Tele a -> Bool #

maximum :: Ord a => Tele a -> a #

minimum :: Ord a => Tele a -> a #

sum :: Num a => Tele a -> a #

product :: Num a => Tele a -> a #

Traversable Tele Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

traverse :: Applicative f => (a -> f b) -> Tele a -> f (Tele b) #

sequenceA :: Applicative f => Tele (f a) -> f (Tele a) #

mapM :: Monad m => (a -> m b) -> Tele a -> m (Tele b) #

sequence :: Monad m => Tele (m a) -> m (Tele a) #

ExpandCase LiftedRep (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Associated Types

type Result LiftedRep (Tele a) 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

type Result LiftedRep (Tele a) = Result LiftedRep (DontExpand (Tele a))

Methods

expand :: ((Tele a -> Result LiftedRep (Tele a)) -> Result LiftedRep (Tele a)) -> Tele a Source #

(t ~ Dom a, Pretty a) => Pretty (Tele t) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

pretty :: Tele t -> Doc Source #

prettyPrec :: Int -> Tele t -> Doc Source #

prettyList :: [Tele t] -> Doc Source #

TermLike a => TermLike (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Tele a -> m (Tele a) Source #

foldTerm :: Monoid m => (Term -> m) -> Tele a -> m Source #

TermLike a => AllMetas (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Tele a -> m Source #

NamesIn a => NamesIn (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Tele a -> m Source #

KillRange a => KillRange (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

killRange :: KillRangeT (Tele a) Source #

Free t => Free (Tele t) Source # 
Instance details

Defined in Mikan.TypeChecking.Free.Generic

Methods

freeVars :: ComputeFree r => Tele t -> Reader r (Collect r) Source #

MentionsMeta a => MentionsMeta (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Tele a -> Bool Source #

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Mikan.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source #

Instantiate t => Instantiate (Tele t) Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiate' :: Tele t -> ReduceM (Tele t) Source #

(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Tele a -> ReduceM (Tele a) Source #

(Subst a, Normalise a) => Normalise (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

normalise' :: Tele a -> ReduceM (Tele a) Source #

(Subst a, Simplify a) => Simplify (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

simplify' :: Tele a -> ReduceM (Tele a)

EmbPrj a => EmbPrj (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Tele a -> S Word32 Source #

icod_ :: Tele a -> S Word32 Source #

value :: Word32 -> R (Tele a) Source #

TermSubst a => Apply (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

apply :: Tele a -> Args -> Tele a Source #

applyE :: Tele a -> Elims -> Tele a Source #

Subst a => Subst (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Associated Types

type SubstArg (Tele a) 
Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg (Tele a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source #

Null (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

empty :: Tele a Source #

null :: Tele a -> Bool Source #

Sized (Tele a) Source #

The size of a telescope is its length (as a list).

Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

size :: Tele a -> Int Source #

natSize :: Tele a -> Peano Source #

NFData a => NFData (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

rnf :: Tele a -> () #

Generic (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Associated Types

type Rep (Tele a) 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

type Rep (Tele a) = D1 ('MetaData "Tele" "Mikan.Syntax.Internal.Telescope" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel#" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 (Abs (Tele a))))))

Methods

from :: Tele a -> Rep (Tele a) x #

to :: Rep (Tele a) x -> Tele a #

Show a => Show (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

showsPrec :: Int -> Tele a -> ShowS #

show :: Tele a -> String #

showList :: [Tele a] -> ShowS #

Eq a => Eq (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

(==) :: Tele a -> Tele a -> Bool #

(/=) :: Tele a -> Tele a -> Bool #

Ord a => Ord (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

compare :: Tele a -> Tele a -> Ordering #

(<) :: Tele a -> Tele a -> Bool #

(<=) :: Tele a -> Tele a -> Bool #

(>) :: Tele a -> Tele a -> Bool #

(>=) :: Tele a -> Tele a -> Bool #

max :: Tele a -> Tele a -> Tele a #

min :: Tele a -> Tele a -> Tele a #

type ReifiesTo Telescope Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope
type Result LiftedRep (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

type Result LiftedRep (Tele a) = Result LiftedRep (DontExpand (Tele a))
type SubstArg (Tele a) Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg (Tele a) = SubstArg a
type Rep (Tele a) Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

type Rep (Tele a) = D1 ('MetaData "Tele" "Mikan.Syntax.Internal.Telescope" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel#" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 (Abs (Tele a))))))

type Telescope = Tele (Dom Type) Source #

mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a Source #

mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #

A traversal for the names in a telescope.

telToArgs :: TelToArgs a => a -> [Arg ArgName] Source #

type ListTel = ListTel' ArgName Source #

type ListTel' a = [Dom (a, Type)] Source #

Telescope as list.

listTel :: Lens' Telescope ListTel Source #

Lens to edit a Telescope as a list.

telToList :: Tele (Dom t) -> [Dom (ArgName, t)] Source #

Convert a telescope to its list form.

This function returns __IMPOSSIBLE__ if it encounters a NoAbs.

telFromList :: ListTel -> Telescope Source #

Convert a list telescope to a telescope.

foldTeleIndices :: (Int -> b -> b) -> b -> Tele a -> b Source #

Fold over the de Bruijn indices of a telescope.

This function returns __IMPOSSIBLE__ if it encounters a NoAbs.

Examples

Expand
>>> foldTeleIndices (:) (ExtendTel () $ Abs "x" $ ExtendTel () $ Abs "y" $ ExtendTel () $ Abs "z" EmptyTel)
[2, 1, 0]

data Teletype Source #

A Teletype represents a Type with some "pending" quantification.

Teletypes are used to avoid the quadratic accumulation of PiSorts when quantifying a type over a telescope, particularly in metavariables.

Teletypes are otherwise identical to Types (by making quantifiers into Pis); teletypes can be operated on transparently by the functions in Mikan.TypeChecking.Telescope.

Constructors

EmptyTt Type

A Type with no quantification.

ExtendTt

A Teletype with an extra domain.

Fields

Instances

Instances details
Pretty Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

pretty :: Teletype -> Doc Source #

prettyPrec :: Int -> Teletype -> Doc Source #

prettyList :: [Teletype] -> Doc Source #

TermLike Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Teletype -> m Teletype Source #

foldTerm :: Monoid m => (Term -> m) -> Teletype -> m Source #

AllMetas Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Teletype -> m Source #

NamesIn Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Teletype -> m Source #

Reify Teletype Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Teletype 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Teletype = Type

Methods

reify :: MonadReify m => Teletype -> m (ReifiesTo Teletype) Source #

reifyWhen :: MonadReify m => Bool -> Teletype -> m (ReifiesTo Teletype) Source #

Free Teletype Source # 
Instance details

Defined in Mikan.TypeChecking.Free.Generic

Methods

freeVars :: ComputeFree r => Teletype -> Reader r (Collect r) Source #

PrettyTCM Teletype Source # 
Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Teletype -> m Doc Source #

InstantiateFull Teletype Source # 
Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Teletype -> ReduceM Teletype Source #

EmbPrj Teletype Source # 
Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Teletype -> S Word32 Source #

icod_ :: Teletype -> S Word32 Source #

value :: Word32 -> R Teletype Source #

Subst Teletype Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

Associated Types

type SubstArg Teletype 
Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg Teletype = Term

Methods

applySubst :: Substitution' (SubstArg Teletype) -> Teletype -> Teletype Source #

NFData Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

rnf :: Teletype -> () #

Generic Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Associated Types

type Rep Teletype 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

type Rep Teletype = D1 ('MetaData "Teletype" "Mikan.Syntax.Internal.Telescope" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "EmptyTt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "ExtendTt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Dom Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 (Abs Teletype))))

Methods

from :: Teletype -> Rep Teletype x #

to :: Rep Teletype x -> Teletype #

Show Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

Methods

showsPrec :: Int -> Teletype -> ShowS #

show :: Teletype -> String #

showList :: [Teletype] -> ShowS #

type ReifiesTo Teletype Source # 
Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Teletype = Type
type SubstArg Teletype Source # 
Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg Teletype = Term
type Rep Teletype Source # 
Instance details

Defined in Mikan.Syntax.Internal.Telescope

type Rep Teletype = D1 ('MetaData "Teletype" "Mikan.Syntax.Internal.Telescope" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "EmptyTt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "ExtendTt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Dom Type)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 (Abs Teletype))))

unpackTeletype :: Teletype -> (Telescope, Type) Source #

Unpack a Teletype into a pair of a Telescope and a Type.

The Type lives under the returned Telescope. Only the quantifiers that belong explicitly to the Teletype are returned in the Telescope: even if the Type has some manifest quantification, it will not be moved into the Telescope.