rzk-0.7.4: An experimental proof assistant for synthetic ∞-categories
Safe HaskellSafe-Inferred
LanguageHaskell2010

Language.Rzk.Free.Syntax

Synopsis

Documentation

data RzkPosition Source #

Constructors

RzkPosition 

Fields

ppRzkPosition :: RzkPosition -> String Source #

newtype VarIdent Source #

Constructors

VarIdent 

Fields

Instances

Instances details
IsString Term' Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

fromString :: String -> Term' #

IsString TermT' Source #

Parse and unsafeInferStandalone'.

Instance details

Defined in Rzk.TypeCheck

Methods

fromString :: String -> TermT' #

IsString VarIdent Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

fromString :: String -> VarIdent #

Show Term' Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

showsPrec :: Int -> Term' -> ShowS #

show :: Term' -> String #

showList :: [Term'] -> ShowS #

Show TermT' Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

showsPrec :: Int -> TermT' -> ShowS #

show :: TermT' -> String #

showList :: [TermT'] -> ShowS #

Show VarIdent Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

showsPrec :: Int -> VarIdent -> ShowS #

show :: VarIdent -> String #

showList :: [VarIdent] -> ShowS #

Eq VarIdent Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

(==) :: VarIdent -> VarIdent -> Bool #

(/=) :: VarIdent -> VarIdent -> Bool #

ppVarIdentWithLocation :: VarIdent -> String Source #

varIdent :: VarIdent -> VarIdent Source #

varIdentAt :: Maybe FilePath -> VarIdent -> VarIdent Source #

fromVarIdent :: VarIdent -> VarIdent Source #

data TermF scope term Source #

Constructors

UniverseF 
UniverseCubeF 
UniverseTopeF 
CubeUnitF 
CubeUnitStarF 
Cube2F 
Cube2_0F 
Cube2_1F 
CubeProductF term term 
TopeTopF 
TopeBottomF 
TopeEQF term term 
TopeLEQF term term 
TopeAndF term term 
TopeOrF term term 
RecBottomF 
RecOrF [(term, term)] 
TypeFunF (Maybe VarIdent) term (Maybe scope) scope 
TypeSigmaF (Maybe VarIdent) term scope 
TypeIdF term (Maybe term) term 
AppF term term 
LambdaF (Maybe VarIdent) (Maybe (term, Maybe scope)) scope 
PairF term term 
FirstF term 
SecondF term 
ReflF (Maybe (term, Maybe term)) 
IdJF term term term term term term 
UnitF 
TypeUnitF 
TypeAscF term term 
TypeRestrictedF term [(term, term)] 

Instances

Instances details
Bifoldable TermF Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

bifold :: Monoid m => TermF m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> TermF a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> TermF a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> TermF a b -> c #

Bifunctor TermF Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

bimap :: (a -> b) -> (c -> d) -> TermF a c -> TermF b d #

first :: (a -> b) -> TermF a c -> TermF b c #

second :: (b -> c) -> TermF a b -> TermF a c #

Bitraversable TermF Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> TermF a b -> f (TermF c d) #

IsString Term' Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

fromString :: String -> Term' #

IsString TermT' Source #

Parse and unsafeInferStandalone'.

Instance details

Defined in Rzk.TypeCheck

Methods

fromString :: String -> TermT' #

Show Term' Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

showsPrec :: Int -> Term' -> ShowS #

show :: Term' -> String #

showList :: [Term'] -> ShowS #

Show TermT' Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

showsPrec :: Int -> TermT' -> ShowS #

show :: TermT' -> String #

showList :: [TermT'] -> ShowS #

Foldable (TermF scope) Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

fold :: Monoid m => TermF scope m -> m #

foldMap :: Monoid m => (a -> m) -> TermF scope a -> m #

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

foldr :: (a -> b -> b) -> b -> TermF scope a -> b #

foldr' :: (a -> b -> b) -> b -> TermF scope a -> b #

foldl :: (b -> a -> b) -> b -> TermF scope a -> b #

foldl' :: (b -> a -> b) -> b -> TermF scope a -> b #

foldr1 :: (a -> a -> a) -> TermF scope a -> a #

foldl1 :: (a -> a -> a) -> TermF scope a -> a #

toList :: TermF scope a -> [a] #

null :: TermF scope a -> Bool #

length :: TermF scope a -> Int #

elem :: Eq a => a -> TermF scope a -> Bool #

maximum :: Ord a => TermF scope a -> a #

minimum :: Ord a => TermF scope a -> a #

sum :: Num a => TermF scope a -> a #

product :: Num a => TermF scope a -> a #

Traversable (TermF scope) Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

sequenceA :: Applicative f => TermF scope (f a) -> f (TermF scope a) #

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

sequence :: Monad m => TermF scope (m a) -> m (TermF scope a) #

Functor (TermF scope) Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

fmap :: (a -> b) -> TermF scope a -> TermF scope b #

(<$) :: a -> TermF scope b -> TermF scope a #

(Eq scope, Eq term) => Eq (TermF scope term) Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

(==) :: TermF scope term -> TermF scope term -> Bool #

(/=) :: TermF scope term -> TermF scope term -> Bool #

pattern TypeRestrictedTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> [(FS (Sum (AnnF ann TermF) g) a, FS (Sum (AnnF ann TermF) g) a)] -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TypeAscTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TypeUnitTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern UnitTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern IdJTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern ReflTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> Maybe (FS (Sum (AnnF ann TermF) g) a, Maybe (FS (Sum (AnnF ann TermF) g) a)) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern SecondTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern FirstTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern PairTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern LambdaTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> Maybe VarIdent -> Maybe (FS (Sum (AnnF ann TermF) g) a, Maybe (Scope (FS (Sum (AnnF ann TermF) g)) a)) -> Scope (FS (Sum (AnnF ann TermF) g)) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern AppTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TypeIdTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> Maybe (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TypeSigmaTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> Maybe VarIdent -> FS (Sum (AnnF ann TermF) g) a -> Scope (FS (Sum (AnnF ann TermF) g)) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TypeFunTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> Maybe VarIdent -> FS (Sum (AnnF ann TermF) g) a -> Maybe (Scope (FS (Sum (AnnF ann TermF) g)) a) -> Scope (FS (Sum (AnnF ann TermF) g)) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern RecOrTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> [(FS (Sum (AnnF ann TermF) g) a, FS (Sum (AnnF ann TermF) g) a)] -> FS (Sum (AnnF ann TermF) g) a Source #

pattern RecBottomTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TopeOrTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TopeAndTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TopeLEQTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TopeEQTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TopeBottomTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TopeTopTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern CubeProductTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a -> FS (Sum (AnnF ann TermF) g) a Source #

pattern Cube2_1TE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern Cube2_0TE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern Cube2TE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern CubeUnitStarTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern CubeUnitTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern UniverseTopeTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern UniverseCubeTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern UniverseTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> FS (Sum (AnnF ann TermF) g) a Source #

pattern TypeRestrictedT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> [(FS (AnnF ann TermF) a, FS (AnnF ann TermF) a)] -> FS (AnnF ann TermF) a Source #

pattern TypeAscT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TypeUnitT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern UnitT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern IdJT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern ReflT :: ann (FS (AnnF ann TermF) a) -> Maybe (FS (AnnF ann TermF) a, Maybe (FS (AnnF ann TermF) a)) -> FS (AnnF ann TermF) a Source #

pattern SecondT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern FirstT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern PairT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern LambdaT :: ann (FS (AnnF ann TermF) a) -> Maybe VarIdent -> Maybe (FS (AnnF ann TermF) a, Maybe (Scope (FS (AnnF ann TermF)) a)) -> Scope (FS (AnnF ann TermF)) a -> FS (AnnF ann TermF) a Source #

pattern AppT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TypeIdT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> Maybe (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TypeSigmaT :: ann (FS (AnnF ann TermF) a) -> Maybe VarIdent -> FS (AnnF ann TermF) a -> Scope (FS (AnnF ann TermF)) a -> FS (AnnF ann TermF) a Source #

pattern TypeFunT :: ann (FS (AnnF ann TermF) a) -> Maybe VarIdent -> FS (AnnF ann TermF) a -> Maybe (Scope (FS (AnnF ann TermF)) a) -> Scope (FS (AnnF ann TermF)) a -> FS (AnnF ann TermF) a Source #

pattern RecOrT :: ann (FS (AnnF ann TermF) a) -> [(FS (AnnF ann TermF) a, FS (AnnF ann TermF) a)] -> FS (AnnF ann TermF) a Source #

pattern RecBottomT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern TopeOrT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TopeAndT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TopeLEQT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TopeEQT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TopeBottomT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern TopeTopT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern CubeProductT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern Cube2_1T :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern Cube2_0T :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern Cube2T :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern CubeUnitStarT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern CubeUnitT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern UniverseTopeT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern UniverseCubeT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern UniverseT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

pattern TypeRestrictedE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> [(FS (Sum TermF g) a, FS (Sum TermF g) a)] -> FS (Sum TermF g) a Source #

pattern TypeAscE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TypeUnitE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern UnitE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern IdJE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern ReflE :: forall {g :: Type -> Type -> Type} {a}. Maybe (FS (Sum TermF g) a, Maybe (FS (Sum TermF g) a)) -> FS (Sum TermF g) a Source #

pattern SecondE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern FirstE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern PairE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern LambdaE :: forall {g :: Type -> Type -> Type} {a}. Maybe VarIdent -> Maybe (FS (Sum TermF g) a, Maybe (Scope (FS (Sum TermF g)) a)) -> Scope (FS (Sum TermF g)) a -> FS (Sum TermF g) a Source #

pattern AppE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TypeIdE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> Maybe (FS (Sum TermF g) a) -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TypeSigmaE :: forall {g :: Type -> Type -> Type} {a}. Maybe VarIdent -> FS (Sum TermF g) a -> Scope (FS (Sum TermF g)) a -> FS (Sum TermF g) a Source #

pattern TypeFunE :: forall {g :: Type -> Type -> Type} {a}. Maybe VarIdent -> FS (Sum TermF g) a -> Maybe (Scope (FS (Sum TermF g)) a) -> Scope (FS (Sum TermF g)) a -> FS (Sum TermF g) a Source #

pattern RecOrE :: forall {g :: Type -> Type -> Type} {a}. [(FS (Sum TermF g) a, FS (Sum TermF g) a)] -> FS (Sum TermF g) a Source #

pattern RecBottomE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern TopeOrE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TopeAndE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TopeLEQE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TopeEQE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TopeBottomE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern TopeTopE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern CubeProductE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern Cube2_1E :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern Cube2_0E :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern Cube2E :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern CubeUnitStarE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern CubeUnitE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern UniverseTopeE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern UniverseCubeE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern UniverseE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

pattern TypeRestricted :: FS TermF a -> [(FS TermF a, FS TermF a)] -> FS TermF a Source #

pattern TypeAsc :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern TypeUnit :: FS TermF a Source #

pattern Unit :: FS TermF a Source #

pattern IdJ :: FS TermF a -> FS TermF a -> FS TermF a -> FS TermF a -> FS TermF a -> FS TermF a -> FS TermF a Source #

pattern Refl :: Maybe (FS TermF a, Maybe (FS TermF a)) -> FS TermF a Source #

pattern Second :: FS TermF a -> FS TermF a Source #

pattern First :: FS TermF a -> FS TermF a Source #

pattern Pair :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern Lambda :: Maybe VarIdent -> Maybe (FS TermF a, Maybe (Scope (FS TermF) a)) -> Scope (FS TermF) a -> FS TermF a Source #

pattern App :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern TypeId :: FS TermF a -> Maybe (FS TermF a) -> FS TermF a -> FS TermF a Source #

pattern TypeSigma :: Maybe VarIdent -> FS TermF a -> Scope (FS TermF) a -> FS TermF a Source #

pattern TypeFun :: Maybe VarIdent -> FS TermF a -> Maybe (Scope (FS TermF) a) -> Scope (FS TermF) a -> FS TermF a Source #

pattern RecOr :: [(FS TermF a, FS TermF a)] -> FS TermF a Source #

pattern RecBottom :: FS TermF a Source #

pattern TopeOr :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern TopeAnd :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern TopeLEQ :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern TopeEQ :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern TopeBottom :: FS TermF a Source #

pattern TopeTop :: FS TermF a Source #

pattern CubeProduct :: FS TermF a -> FS TermF a -> FS TermF a Source #

pattern Cube2_1 :: FS TermF a Source #

pattern Cube2_0 :: FS TermF a Source #

pattern Cube2 :: FS TermF a Source #

pattern CubeUnitStar :: FS TermF a Source #

pattern CubeUnit :: FS TermF a Source #

pattern UniverseTope :: FS TermF a Source #

pattern UniverseCube :: FS TermF a Source #

pattern Universe :: FS TermF a Source #

newtype Type term Source #

Constructors

Type 

Fields

Instances

Instances details
Foldable Type Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

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

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

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

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

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

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

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

toList :: Type a -> [a] #

null :: Type a -> Bool #

length :: Type a -> Int #

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

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

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

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

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

Traversable Type Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

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

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

Functor Type Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

Eq term => Eq (Type term) Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

(==) :: Type term -> Type term -> Bool #

(/=) :: Type term -> Type term -> Bool #

data TypeInfo term Source #

Constructors

TypeInfo 

Fields

Instances

Instances details
Foldable TypeInfo Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

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

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

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

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

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

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

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

toList :: TypeInfo a -> [a] #

null :: TypeInfo a -> Bool #

length :: TypeInfo a -> Int #

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

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

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

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

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

IsString TermT' Source #

Parse and unsafeInferStandalone'.

Instance details

Defined in Rzk.TypeCheck

Methods

fromString :: String -> TermT' #

Traversable TypeInfo Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

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

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

Functor TypeInfo Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

Show TermT' Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

showsPrec :: Int -> TermT' -> ShowS #

show :: TermT' -> String #

showList :: [TermT'] -> ShowS #

Eq term => Eq (TypeInfo term) Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

(==) :: TypeInfo term -> TypeInfo term -> Bool #

(/=) :: TypeInfo term -> TypeInfo term -> Bool #

type Term = FS TermF Source #

type TermT = FS (AnnF TypeInfo TermF) Source #

termIsWHNF :: TermT var -> TermT var Source #

termIsNF :: TermT var -> TermT var Source #

invalidateWHNF :: TermT var -> TermT var Source #

substituteT :: TermT var -> Scope TermT var -> TermT var Source #

type Term' = Term VarIdent Source #

type TermT' = TermT VarIdent Source #

freeVars :: Term a -> [a] Source #

partialFreeVarsT :: TermT a -> [a] Source #

freeVarsT :: Eq a => (a -> TermT a) -> TermT a -> [a] Source #

toTerm' :: Term -> Term' Source #

toScope :: VarIdent -> (VarIdent -> Term a) -> Term -> Scope Term a Source #

toScopePattern :: Pattern -> (VarIdent -> Term a) -> Term -> Scope Term a Source #

toTerm :: (VarIdent -> Term a) -> Term -> Term a Source #

patternToTerm :: Pattern -> Term Source #

unsafeTermToPattern :: Term -> Pattern Source #

fromTerm' :: Term' -> Term Source #

fromScope' :: VarIdent -> [VarIdent] -> [VarIdent] -> Scope Term VarIdent -> Term Source #

fromTermWith' :: [VarIdent] -> [VarIdent] -> Term' -> Term Source #

defaultVarIdents :: [VarIdent] Source #

refreshVar :: [VarIdent] -> VarIdent -> VarIdent Source #

Given a list of used variable names in the current context, generate a unique fresh name based on a given one.

>>> print $ refreshVar ["x", "y", "x₁", "z"] "x"
x₂

incVarIdentIndex :: VarIdent -> VarIdent Source #

incIndex :: String -> String Source #

Increment the subscript number at the end of the indentifier.

>>> putStrLn $ incIndex "x"
x₁
>>> putStrLn $ incIndex "x₁₉"
x₂₀