Agda.TypeChecking.Rules.LHS.Unify.Types

Documentation

data Equality

Constructors

Equal

Fields

• _eqType :: Dom Type
• _eqLeft :: Term
• _eqRight :: Term

eqConstructorForm :: HasBuiltins m => Equality -> m Equality

eqUnLevel :: HasBuiltins m => Equality -> m Equality

data UnifyState

Constructors

UState

Fields

• varTel :: Telescope

  Don't reduce!

• flexVars :: FlexibleVars
• eqTel :: Telescope

  Can be reduced eagerly.

• eqLHS :: [Arg Term]

  Ends up in dot patterns (should not be reduced eagerly).

• eqRHS :: [Arg Term]

  Ends up in dot patterns (should not be reduced eagerly).

Instances

PrettyTCM UnifyState

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

Methods

prettyTCM :: MonadPretty m => UnifyState -> m Doc

Reduce UnifyState

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.

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

Methods

reduce' :: UnifyState -> ReduceM UnifyState

reduceB' :: UnifyState -> ReduceM (Blocked UnifyState)

Show UnifyState

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

Methods

showsPrec :: Int -> UnifyState -> ShowS

show :: UnifyState -> String

showList :: [UnifyState] -> ShowS

lensVarTel :: Lens' Telescope UnifyState

lensEqTel :: Lens' Telescope UnifyState

initUnifyState :: PureTCM m => Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState

isUnifyStateSolved :: UnifyState -> Bool

varCount :: UnifyState -> Int

getVarType :: Int -> UnifyState -> Dom Type

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

getVarTypeUnraised :: Int -> UnifyState -> Dom Type

eqCount :: UnifyState -> Int

getEquality :: Int -> UnifyState -> Equality

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

getReducedEquality :: (MonadReduce m, MonadAddContext m) => Int -> UnifyState -> m Equality

getEqualityUnraised :: Int -> UnifyState -> Equality

As getEquality, but with the unraised type

getReducedEqualityUnraised :: (MonadReduce m, MonadAddContext m) => Int -> UnifyState -> m Equality

solveVar

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.

applyUnder :: Int -> Telescope -> Term -> Telescope

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

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

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

data UnifyStep

Constructors

Deletion

Fields

• deleteAt :: Int
• deleteType :: Type
• deleteLeft :: Term
• deleteRight :: Term

Solution

Fields

• solutionAt :: Int
• solutionType :: Dom Type
• solutionVar :: FlexibleVar Int
• solutionTerm :: Term
• solutionSide :: Either () ()

  side of the equation where the variable is.

Injectivity

Fields

• injectAt :: Int
• injectType :: Type
• injectDatatype :: QName
• injectParameters :: Args
• injectIndices :: Args
• injectConstructor :: ConHead

Conflict

Fields

• conflictAt :: Int
• conflictType :: Type
• conflictDatatype :: QName
• conflictParameters :: Args
• conflictLeft :: Term
• conflictRight :: Term

Cycle

Fields

• cycleAt :: Int
• cycleType :: Type
• cycleDatatype :: QName
• cycleParameters :: Args
• cycleVar :: Int
• cycleOccursIn :: Term

EtaExpandVar

Fields

• expandVar :: FlexibleVar Int
• expandVarRecordType :: QName
• expandVarParameters :: Args

EtaExpandEquation

Fields

• expandAt :: Int
• expandRecordType :: QName
• expandParameters :: Args

LitConflict

Fields

• litConflictAt :: Int
• litType :: Type
• litConflictLeft :: Literal
• litConflictRight :: Literal

StripSizeSuc

Fields

• stripAt :: Int
• stripArgLeft :: Term
• stripArgRight :: Term

SkipIrrelevantEquation

Fields

• skipIrrelevantAt :: Int

TypeConInjectivity

Fields

• typeConInjectAt :: Int
• typeConstructor :: QName
• typeConArgsLeft :: Args
• typeConArgsRight :: Args

Instances

PrettyTCM UnifyStep

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

Methods

prettyTCM :: MonadPretty m => UnifyStep -> m Doc

Show UnifyStep

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

Methods

showsPrec :: Int -> UnifyStep -> ShowS

show :: UnifyStep -> String

showList :: [UnifyStep] -> ShowS

data UnifyLogEntry

Constructors

UnificationStep UnifyState UnifyStep UnifyOutput

type UnifyLog = [(UnifyLogEntry, UnifyState)]

type UnifyLog' = DList (UnifyLogEntry, UnifyState)

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

data UnifyOutput

Constructors

UnifyOutput

Fields

• unifySubst :: PatternSubstitution
• unifyProof :: PatternSubstitution

Instances

Monoid UnifyOutput

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

Methods

mempty :: UnifyOutput

mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput

mconcat :: [UnifyOutput] -> UnifyOutput

Semigroup UnifyOutput

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

Methods

(<>) :: UnifyOutput -> UnifyOutput -> UnifyOutput

sconcat :: NonEmpty UnifyOutput -> UnifyOutput

stimes :: Integral b => b -> UnifyOutput -> UnifyOutput

type UnifyLogT m a = WriterT UnifyLog' m a

type UnifyStepT m a = WriterT UnifyOutput m a

tellUnifySubst :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()

tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()

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

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