Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rules.LHS.Unify.Types

Synopsis

Documentation

data Equality Source #

Constructors

Equal 

Fields

data UnifyState Source #

Constructors

UState 

Fields

Instances

Instances details
PrettyTCM UnifyState Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Reduce UnifyState Source #

Don't ever reduce the whole varTel, as it will destroy readability of the context in interactive editing! To make sure this insight is not lost, the following dummy instance should prevent a proper Reduce instance for UnifyState.

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Show UnifyState Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Methods

showsPrec :: Int -> UnifyState -> ShowS

show :: UnifyState -> String

showList :: [UnifyState] -> ShowS

getVarType :: Int -> UnifyState -> Dom Type Source #

Get the type of the i'th variable in the given state

getEquality :: Int -> UnifyState -> Equality Source #

Get the k'th equality in the given state. The left- and right-hand sides of the equality live in the varTel telescope, and the type of the equality lives in the varTel++eqTel telescope

getEqualityUnraised :: Int -> UnifyState -> Equality Source #

As getEquality, but with the unraised type

solveVar Source #

Arguments

:: Int

Index k

-> DeBruijnPattern

Solution u

-> UnifyState 
-> Maybe (UnifyState, PatternSubstitution) 

Instantiate the k'th variable with the given value. Returns Nothing if there is a cycle.

dropAt :: Int -> [a] -> [a] Source #

solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution) Source #

Solve the k'th equation with the given value, which can depend on regular variables but not on other equation variables.

data UnifyStep Source #

Instances

Instances details
PrettyTCM UnifyStep Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Show UnifyStep Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Methods

showsPrec :: Int -> UnifyStep -> ShowS

show :: UnifyStep -> String

showList :: [UnifyStep] -> ShowS

type UnifyLog' = DList (UnifyLogEntry, UnifyState) Source #

This variant of UnifyLog is used to ensure that tell is not expensive.

type UnifyLogT (m :: Type -> Type) a = WriterT UnifyLog' m a Source #

type UnifyStepT (m :: Type -> Type) a = WriterT UnifyOutput m a Source #

writeUnifyLog :: MonadWriter UnifyLog' m => (UnifyLogEntry, UnifyState) -> m () Source #

runUnifyLogT :: Functor m => UnifyLogT m a -> m (a, UnifyLog) Source #