Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Equality = Equal {}
- eqConstructorForm :: HasBuiltins m => Equality -> m Equality
- eqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality
- data UnifyState = UState {}
- lensVarTel :: Lens' UnifyState Telescope
- lensEqTel :: Lens' UnifyState Telescope
- initUnifyState :: PureTCM m => Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState
- isUnifyStateSolved :: UnifyState -> Bool
- varCount :: UnifyState -> Int
- getVarType :: Int -> UnifyState -> Dom Type
- getVarTypeUnraised :: Int -> UnifyState -> Dom Type
- eqCount :: UnifyState -> Int
- getEquality :: Int -> UnifyState -> Equality
- getReducedEquality :: (MonadReduce m, MonadAddContext m) => Int -> UnifyState -> m Equality
- getEqualityUnraised :: Int -> UnifyState -> Equality
- getReducedEqualityUnraised :: (MonadReduce m, MonadAddContext m) => Int -> UnifyState -> m Equality
- solveVar :: Int -> DeBruijnPattern -> UnifyState -> Maybe (UnifyState, PatternSubstitution)
- applyUnder :: Int -> Telescope -> Term -> Telescope
- dropAt :: Int -> [a] -> [a]
- solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
- data UnifyStep
- = Deletion {
- deleteAt :: Int
- deleteType :: Type
- deleteLeft :: Term
- deleteRight :: Term
- | Solution {
- solutionAt :: Int
- solutionType :: Dom Type
- solutionVar :: FlexibleVar Int
- solutionTerm :: Term
- solutionSide :: Either () ()
- | Injectivity {
- injectAt :: Int
- injectType :: Type
- injectDatatype :: QName
- injectParameters :: Args
- injectIndices :: Args
- injectConstructor :: ConHead
- | Conflict {
- conflictAt :: Int
- conflictType :: Type
- conflictDatatype :: QName
- conflictParameters :: Args
- conflictLeft :: Term
- conflictRight :: Term
- | Cycle {
- cycleAt :: Int
- cycleType :: Type
- cycleDatatype :: QName
- cycleParameters :: Args
- cycleVar :: Int
- cycleOccursIn :: Term
- | EtaExpandVar { }
- | EtaExpandEquation {
- expandAt :: Int
- expandRecordType :: QName
- expandParameters :: Args
- | LitConflict {
- litConflictAt :: Int
- litType :: Type
- litConflictLeft :: Literal
- litConflictRight :: Literal
- | StripSizeSuc {
- stripAt :: Int
- stripArgLeft :: Term
- stripArgRight :: Term
- | SkipIrrelevantEquation {
- skipIrrelevantAt :: Int
- | TypeConInjectivity {
- typeConInjectAt :: Int
- typeConstructor :: QName
- typeConArgsLeft :: Args
- typeConArgsRight :: Args
- = Deletion {
- data UnifyLogEntry = UnificationStep UnifyState UnifyStep UnifyOutput
- type UnifyLog = [(UnifyLogEntry, UnifyState)]
- type UnifyLog' = DList (UnifyLogEntry, UnifyState)
- data UnifyOutput = UnifyOutput {}
- type UnifyLogT (m :: Type -> Type) a = WriterT UnifyLog' m a
- type UnifyStepT (m :: Type -> Type) 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)
Documentation
eqConstructorForm :: HasBuiltins m => Equality -> m Equality Source #
eqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality Source #
data UnifyState Source #
Instances
PrettyTCM UnifyState Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Unify.Types prettyTCM :: MonadPretty m => UnifyState -> m Doc Source # | |
Reduce UnifyState Source # | Don't ever reduce the whole |
Defined in Agda.TypeChecking.Rules.LHS.Unify.Types reduce' :: UnifyState -> ReduceM UnifyState Source # reduceB' :: UnifyState -> ReduceM (Blocked UnifyState) Source # | |
Show UnifyState Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Unify.Types showsPrec :: Int -> UnifyState -> ShowS show :: UnifyState -> String showList :: [UnifyState] -> ShowS |
initUnifyState :: PureTCM m => Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState Source #
isUnifyStateSolved :: UnifyState -> Bool Source #
varCount :: UnifyState -> Int Source #
getVarType :: Int -> UnifyState -> Dom Type Source #
Get the type of the i'th variable in the given state
getVarTypeUnraised :: Int -> UnifyState -> Dom Type Source #
eqCount :: UnifyState -> Int Source #
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
getReducedEquality :: (MonadReduce m, MonadAddContext m) => Int -> UnifyState -> m Equality Source #
getEqualityUnraised :: Int -> UnifyState -> Equality Source #
As getEquality, but with the unraised type
getReducedEqualityUnraised :: (MonadReduce m, MonadAddContext m) => Int -> UnifyState -> m Equality Source #
:: Int | Index |
-> DeBruijnPattern | Solution |
-> UnifyState | |
-> Maybe (UnifyState, PatternSubstitution) |
Instantiate the k'th variable with the given value. Returns Nothing if there is a cycle.
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.
type UnifyLog = [(UnifyLogEntry, UnifyState)] Source #
type UnifyLog' = DList (UnifyLogEntry, UnifyState) Source #
This variant of UnifyLog
is used to ensure that tell
is not
expensive.
data UnifyOutput Source #
Instances
Monoid UnifyOutput Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Unify.Types mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput mconcat :: [UnifyOutput] -> UnifyOutput | |
Semigroup UnifyOutput Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Unify.Types (<>) :: UnifyOutput -> UnifyOutput -> UnifyOutput # sconcat :: NonEmpty UnifyOutput -> UnifyOutput stimes :: Integral b => b -> UnifyOutput -> UnifyOutput |
type UnifyStepT (m :: Type -> Type) a = WriterT UnifyOutput m a Source #
tellUnifySubst :: MonadWriter UnifyOutput m => PatternSubstitution -> m () Source #
tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m () Source #
writeUnifyLog :: MonadWriter UnifyLog' m => (UnifyLogEntry, UnifyState) -> m () Source #
runUnifyLogT :: Functor m => UnifyLogT m a -> m (a, UnifyLog) Source #