Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Rules.LHS.Unify.Types

Synopsis

data Equality = Equal {
- _eqType :: Dom Type
- _eqLeft :: Term
- _eqRight :: Term
}
eqConstructorForm :: HasBuiltins m => Equality -> m Equality
eqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality
data UnifyState = UState {
- varTel :: Telescope
- flexVars :: FlexibleVars
- eqTel :: Telescope
- eqLHS :: [Arg Term]
- eqRHS :: [Arg Term]
}
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 {
  - 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
  }
data UnifyLogEntry = UnificationStep UnifyState UnifyStep UnifyOutput
type UnifyLog = [(UnifyLogEntry, UnifyState)]
type UnifyLog' = DList (UnifyLogEntry, UnifyState)
data UnifyOutput = UnifyOutput {
- unifySubst :: PatternSubstitution
- unifyProof :: PatternSubstitution
}
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

data Equality Source #

Constructors

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

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

eqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality Source #

data UnifyState Source #

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

Instances details

PrettyTCM UnifyState Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods prettyTCM :: MonadPretty m => UnifyState -> m Doc Source #
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 Methods reduce' :: UnifyState -> ReduceM UnifyState Source # reduceB' :: UnifyState -> ReduceM (Blocked UnifyState) Source #
Show UnifyState Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods showsPrec :: Int -> UnifyState -> ShowS show :: UnifyState -> String showList :: [UnifyState] -> ShowS

lensVarTel :: Lens' UnifyState Telescope Source #

lensEqTel :: Lens' UnifyState Telescope Source #

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 #

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.

applyUnder :: Int -> Telescope -> Term -> Telescope Source #

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 #

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

Instances details

PrettyTCM UnifyStep Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods prettyTCM :: MonadPretty m => UnifyStep -> m Doc Source #
Show UnifyStep Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods showsPrec :: Int -> UnifyStep -> ShowS show :: UnifyStep -> String showList :: [UnifyStep] -> ShowS

data UnifyLogEntry Source #

Constructors

UnificationStep UnifyState UnifyStep UnifyOutput

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 #

Constructors

UnifyOutput
Fields unifySubst :: PatternSubstitution unifyProof :: PatternSubstitution

Instances

Instances details

Monoid UnifyOutput Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods mempty :: UnifyOutput mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput mconcat :: [UnifyOutput] -> UnifyOutput
Semigroup UnifyOutput Source #
Instance details 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 :: Type -> Type) a = WriterT UnifyLog' m a Source #

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 #