Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 Source # show :: UnifyState -> String Source # showList :: [UnifyState] -> ShowS Source #

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 Source # show :: UnifyStep -> String Source # showList :: [UnifyStep] -> ShowS Source #

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 Source # mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput Source # mconcat :: [UnifyOutput] -> UnifyOutput Source #
Semigroup UnifyOutput Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.Types Methods (<>) :: UnifyOutput -> UnifyOutput -> UnifyOutput Source # sconcat :: NonEmpty UnifyOutput -> UnifyOutput Source # stimes :: Integral b => b -> UnifyOutput -> UnifyOutput Source #

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 #