rzk-0.9.1: An experimental proof assistant for synthetic ∞-categories
Safe HaskellNone
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 #

holeName :: Text -> Maybe VarIdent Source #

The display name of a hole from its surface token text. The token includes the leading ?; an anonymous hole (bare ?) has no name.

holeIdentToken :: Maybe VarIdent -> Text Source #

The surface token text (including the leading ?) for a hole name.

data Binder Source #

The name(s) a binder introduces. A binder may name a single (possibly anonymous) variable, or destructure a pair/tuple via a pattern. The pattern structure is kept around purely so that goals, holes and error messages can show the user's original names (e.g. t and s for \ (t , s) -> …) instead of projections of a fresh variable (e.g. π₁ x₄ and π₂ x₄).

Operationally a pair pattern still binds a single variable; the components are projections of it (see toScopePattern). Binder only records the names so they can be restored when rendering.

Constructors

BinderVar (Maybe VarIdent)

a single variable (Nothing for _)

BinderPair Binder Binder

a pair pattern (l , r)

BinderUnit

the unit pattern unit

Instances

Instances details
Eq Binder Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

binderName :: Binder -> Maybe VarIdent Source #

The single name of a binder, if it binds exactly one named variable. A pair/unit pattern has no single name, so this is Nothing for them. Used wherever the old Maybe VarIdent binder name is still sufficient.

data TModality Source #

Constructors

Sharp 
Flat 
Op 
Id 

Instances

Instances details
Show TModality Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

showsPrec :: Int -> TModality -> ShowS #

show :: TModality -> String #

showList :: [TModality] -> ShowS #

Eq TModality Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

ModeTheory TModality Source # 
Instance details

Defined in Rzk.TypeCheck

Methods

iden :: TModality Source #

comp :: TModality -> TModality -> TModality Source #

coe :: TModality -> TModality -> Bool Source #

isRA :: TModality -> Bool Source #

toModality :: Modality -> TModality Source #

modCompToMods :: ModComp -> (TModality, TModality) Source #

fromMod :: TModality -> Modality Source #

modsToModComp :: TModality -> TModality -> ModComp Source #

data TermF scope term Source #

Constructors

UniverseF 
UniverseCubeF 
UniverseTopeF 
CubeUnitF 
CubeUnitStarF 
Cube2F 
Cube2_0F 
Cube2_1F 
CubeIF 
CubeI_0F 
CubeI_1F 
CubeProductF term term 
CubeFlipF term 
CubeUnflipF term 
TopeTopF 
TopeBottomF 
TopeEQF term term 
TopeLEQF term term 
TopeAndF term term 
TopeOrF term term 
TopeInvF term 
TopeUninvF term 
RecBottomF 
RecOrF [(term, term)] 
TypeFunF Binder TModality term (Maybe scope) scope 
TypeSigmaF Binder TModality term scope 
TypeIdF term (Maybe term) term 
AppF term term 
LetF Binder (Maybe term) term scope 
LambdaF Binder (Maybe (TModality, 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)] 
TypeModalF TModality term 
ModAppF TModality term 
ModExtractF TModality TModality term 
LetModF Binder TModality TModality (Maybe term) term scope 
HoleF (Maybe VarIdent) 

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 #

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 #

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) #

(Eq term, Eq scope) => 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 HoleTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> Maybe VarIdent -> FS (Sum (AnnF ann TermF) g) a Source #

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

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

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

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

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) -> Binder -> Maybe (TModality, 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 LetTE :: forall {ann} {g :: Type -> Type -> Type} {a}. ann (FS (Sum (AnnF ann TermF) g) a) -> Binder -> Maybe (FS (Sum (AnnF ann TermF) g) a) -> 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) -> Binder -> TModality -> 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) -> Binder -> TModality -> 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 TopeUninvTE :: 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 TopeInvTE :: 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 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 CubeUnflipTE :: 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 CubeFlipTE :: 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 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 CubeI_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 CubeI_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 CubeITE :: 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_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 HoleT :: ann (FS (AnnF ann TermF) a) -> Maybe VarIdent -> FS (AnnF ann TermF) a Source #

pattern LetModT :: ann (FS (AnnF ann TermF) a) -> Binder -> TModality -> TModality -> Maybe (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> Scope (FS (AnnF ann TermF)) a -> FS (AnnF ann TermF) a Source #

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

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

pattern TypeModalT :: ann (FS (AnnF ann TermF) a) -> TModality -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) 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) -> Binder -> Maybe (TModality, 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 LetT :: ann (FS (AnnF ann TermF) a) -> Binder -> Maybe (FS (AnnF ann TermF) a) -> 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) -> Binder -> TModality -> 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) -> Binder -> TModality -> 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 TopeUninvT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern TopeInvT :: ann (FS (AnnF ann TermF) a) -> 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 CubeUnflipT :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a -> FS (AnnF ann TermF) a Source #

pattern CubeFlipT :: ann (FS (AnnF ann TermF) a) -> 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 CubeI_1T :: ann (FS (AnnF ann TermF) a) -> FS (AnnF ann TermF) a Source #

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

pattern CubeIT :: ann (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 HoleE :: forall {g :: Type -> Type -> Type} {a}. Maybe VarIdent -> FS (Sum TermF g) a Source #

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

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

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

pattern TypeModalE :: forall {g :: Type -> Type -> Type} {a}. TModality -> FS (Sum TermF g) a -> FS (Sum TermF g) 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}. Binder -> Maybe (TModality, 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 LetE :: forall {g :: Type -> Type -> Type} {a}. Binder -> Maybe (FS (Sum TermF g) a) -> 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}. Binder -> TModality -> 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}. Binder -> TModality -> 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 TopeUninvE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern TopeInvE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) 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 CubeUnflipE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a -> FS (Sum TermF g) a Source #

pattern CubeFlipE :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) 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 CubeI_1E :: forall {g :: Type -> Type -> Type} {a}. FS (Sum TermF g) a Source #

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

pattern CubeIE :: forall {g :: Type -> Type -> Type} {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 Hole :: Maybe VarIdent -> FS TermF a Source #

pattern LetMod :: Binder -> TModality -> TModality -> Maybe (FS TermF a) -> FS TermF a -> Scope (FS TermF) a -> FS TermF a Source #

pattern ModExtract :: TModality -> TModality -> FS TermF a -> FS TermF a Source #

pattern ModApp :: TModality -> FS TermF a -> FS TermF a Source #

pattern TypeModal :: TModality -> FS TermF a -> FS TermF 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 :: Binder -> Maybe (TModality, FS TermF a, Maybe (Scope (FS TermF) a)) -> Scope (FS TermF) a -> FS TermF a Source #

pattern Let :: Binder -> Maybe (FS TermF a) -> 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 :: Binder -> TModality -> FS TermF a -> Scope (FS TermF) a -> FS TermF a Source #

pattern TypeFun :: Binder -> TModality -> 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 TopeUninv :: FS TermF a -> FS TermF a Source #

pattern TopeInv :: FS TermF a -> 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 CubeUnflip :: FS TermF a -> FS TermF a Source #

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

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

pattern CubeI_1 :: FS TermF a Source #

pattern CubeI_0 :: FS TermF a Source #

pattern CubeI :: 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
Functor Type Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

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) #

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
Functor TypeInfo Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

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) #

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 #

desugarTuple :: t -> [Pattern' t] -> Pattern' t -> Pattern' t -> Pattern' t Source #

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

patternToTerm :: Pattern -> Term Source #

modalColonModality :: ModalColon -> Modality Source #

modalColonToTModality :: ModalColon -> TModality Source #

fromTModalityToModalColon :: TModality -> ModalColon Source #

flattenBinderApp :: Term -> [Term] Source #

Split a binder term into the individual variables it names. A multi-variable binder like (x y : A) is parsed as the application spine x y; this returns [x, y] so each can become its own nested binder. A single binder term (a variable, a pair pattern, …) is returned unchanged as a singleton.

unsafeTermToPattern :: Term -> Pattern Source #

sigmaParamToTypeSigma :: BNFC'Position -> SigmaParam -> Term -> Term Source #

data Proj Source #

A projection step: first (π₁) or second (π₂) component.

Constructors

PFst 
PSnd 

Instances

Instances details
Eq Proj Source # 
Instance details

Defined in Language.Rzk.Free.Syntax

Methods

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

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

binderToPattern :: Binder -> Pattern Source #

Render a Binder as a surface pattern (used to display the binder itself, e.g. (t , s)). Anonymous variables become _.

binderToTerm :: Binder -> Term VarIdent Source #

A term that prints as the binder's surface pattern, e.g. the point (t , s). Used to render a bare occurrence of a pattern binder's variable (one not under a projection, e.g. the point in a shape tope Δ² (t , s)) as the pattern itself rather than the underlying single variable. A single-variable binder yields that variable.

binderDisplayName :: Binder -> VarIdent Source #

A VarIdent that prints as the binder's surface pattern, e.g. (t , s). Used to display a pattern binder in a hole's local context as the pattern itself rather than as the underlying single variable.

binderPaths :: Binder -> [([Proj], VarIdent)] Source #

The named leaves of a binder, each paired with the projection path that reaches it from the bound variable. For example (t , (a , b)) yields [([PFst], t), ([PSnd, PFst], a), ([PSnd, PSnd], b)].

binderLeaves :: Binder -> [VarIdent] Source #

The names appearing in a binder.

binderIsCompound :: Binder -> Bool Source #

Does this binder destructure a pair/tuple (as opposed to naming a single variable or _)?

freshenBinderLeaves :: [VarIdent] -> Binder -> Binder Source #

Refresh the named leaves of a binder so they avoid the given names (and one another). Anonymous leaves and the unit pattern are left unchanged.

projChain :: Term a -> Maybe ([Proj], a) Source #

Decompose a chain of projections applied to a variable into the projection path from the variable outwards, matching binderPaths. The outermost projection is applied last, so it goes at the end of the path: e.g. π₂ (π₁ x) (select π₁ first, then π₂) becomes Just ([PFst, PSnd], x).

foldBinderProjections :: Eq a => [(a, [([Proj], a)])] -> Term a -> Term a Source #

Replace projection chains rooted at a pattern binder with the binder's component name. Given a map from a (bound) variable to the named leaves of its binder, every π₁/π₂ chain that reaches a named leaf is rewritten to that name. Ordinary projections (of variables not bound by a pattern, or chains that do not reach a named leaf) are left untouched.

restorePatternVars :: [(VarIdent, Binder)] -> Term VarIdent -> Term VarIdent Source #

Replace bare uses of a pattern binder's variable with the pattern term (e.g. a whole point (t , s) rather than the underlying single variable, in a tope Δ² (t , s)). Given a map from each (already display-named) variable to its binder, every free occurrence of a compound binder's variable is expanded to its pattern. Complements foldBinderProjections, which folds projections of such a variable; run this after folding, so projections have already become component names and only bare uses remain.

projChainT :: TermT a -> Maybe ([Proj], a) Source #

Like projChain, but for type-annotated terms.

foldBinderProjectionsT :: Eq a => [(a, [([Proj], a)])] -> TermT a -> TermT a Source #

Like foldBinderProjections, but for type-annotated terms (e.g. those embedded in type errors). The annotation of a folded leaf is dropped, which is harmless: the result is only rendered, and a bare variable needs none.

fromTerm' :: Term' -> Term Source #

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

fromScopeBinder' :: Binder -> VarIdent -> [VarIdent] -> [VarIdent] -> Scope Term VarIdent -> Term Source #

Like fromScope', but additionally restores pattern-binder component names inside the scope: projections of the bound variable x are folded back to the names recorded in binder (e.g. π₁ x becomes t). For a binder that names a single variable this is exactly fromScope'.

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

defaultVarIdents :: [VarIdent] Source #

>>> :set -XOverloadedStrings
>>> import qualified Data.Text as T

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 :: Text -> Text Source #

Increment the subscript number at the end of the indentifier.

>>> putStrLn $ T.unpack $ incIndex "x"
x₁
>>> putStrLn $ T.unpack $ incIndex "x₁₉"
x₂₀