ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Rules.LHS.Unify.Types

9 types
22 values

PackageAgda-2.7.0.1
Exports31
LanguageHaskell2010
LicenceMIT
SourceTypes.hs

datadata Equality

Constructors

Equal
- _eqType :: Dom Type
- _eqLeft :: Term
- _eqRight :: Term

valueeqConstructorForm :: HasBuiltins m => Equality -> m Equality

valueeqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality

datadata UnifyState

Constructors

UState
- 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).

Instances3Show, PrettyTCM, Reduce

Show UnifyStateDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.Types
PrettyTCM UnifyStateDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.Types
Reduce UnifyStateDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.Types
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.

valuelensVarTel :: Lens' UnifyState Telescope

valuelensEqTel :: Lens' UnifyState Telescope

valueinitUnifyState

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

valueisUnifyStateSolved :: UnifyState -> Bool

valuevarCount :: UnifyState -> Int

valuegetVarType :: Int -> UnifyState -> Dom Type

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

valuegetVarTypeUnraised :: Int -> UnifyState -> Dom Type

valueeqCount :: UnifyState -> Int

valuegetEquality :: 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

valuegetReducedEquality

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

valuegetEqualityUnraised :: Int -> UnifyState -> Equality

As getEquality, but with the unraised type

valuegetReducedEqualityUnraised

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

valuesolveVar

:: 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.

valueapplyUnder :: Int -> Telescope -> Term -> Telescope

valuedropAt :: Int -> [a] -> [a]

valuesolveEq :: 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.

datadata UnifyStep

Constructors

Deletion
- deleteAt :: Int
- deleteType :: Type
- deleteLeft :: Term
- deleteRight :: Term
Solution
- solutionAt :: Int
- solutionType :: Dom Type
- solutionVar :: FlexibleVar Int
- solutionTerm :: Term
- solutionSide :: Either () ()
  side of the equation where the variable is.
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
- expandVar :: FlexibleVar Int
- expandVarRecordType :: QName
- expandVarParameters :: Args
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

Instances2Show, PrettyTCM

Show UnifyStepDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.Types
PrettyTCM UnifyStepDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.Types

datadata UnifyLogEntry

Constructors

UnificationStep UnifyState UnifyStep UnifyOutput

typetype UnifyLog = [(UnifyLogEntry, UnifyState)]

typetype UnifyLog' = DList (UnifyLogEntry, UnifyState)

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

datadata UnifyOutput

Constructors

UnifyOutput
- unifySubst :: PatternSubstitution
- unifyProof :: PatternSubstitution

Instances2Semigroup, Monoid

Semigroup UnifyOutputDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.Types
Monoid UnifyOutputDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.Types

typetype UnifyLogT (m :: Type -> Type) a = WriterT UnifyLog' m a

typetype UnifyStepT (m :: Type -> Type) a = WriterT UnifyOutput m a

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

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

valuewriteUnifyLog

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

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