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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.LHS.Unify

Description

Unification algorithm for specializing datatype indices, as described in "Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data" by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2016).

This is the unification algorithm used for checking the left-hand side of clauses (see `Agda.TypeChecking.Rules.LHS`), coverage checking (see `Agda.TypeChecking.Coverage`) and indirectly also for interactive case splitting (see `Agda.Interaction.MakeCase`).

A unification problem (of type `UnifyState`) consists of: 1. A telescope `varTel` of free variables, some or all of which are flexible (as indicated by `flexVars`). 2. A telescope `eqTel` containing the types of the equations. 3. Left- and right-hand sides for each equation: `varTel ⊢ eqLHS : eqTel` and `varTel ⊢ eqRHS : eqTel`.

The unification algorithm can end in three different ways: (type `UnificationResult`): - A *positive success* `Unifies (tel, sigma, ps)` with `tel ⊢ sigma : varTel`, `tel ⊢ eqLHS [ varTel ↦ sigma ] ≡ eqRHS [ varTel ↦ sigma ] : eqTel`, and `tel ⊢ ps : eqTel`. In this case, `sigma;ps` is an *equivalence* between the telescopes `tel` and `varTel(eqLHS ≡ eqRHS)`. - A *negative success* `NoUnify err` means that a conflicting equation was found (e.g an equation between two distinct constructors or a cycle). - A *failure* `DontKnow err` means that the unifier got stuck.

The unification algorithm itself consists of two parts: 1. A *unification strategy* takes a unification problem and produces a list of suggested unification rules (of type `UnifyStep`). Strategies can be constructed by composing simpler strategies (see for example the definition of `completeStrategyAt`). 2. The *unification engine* `unifyStep` takes a unification rule and tries to apply it to the given state, writing the result to the UnifyOutput on a success.

The unification steps (of type `UnifyStep`) are the following: - *Deletion* removes a reflexive equation `u =?= v : a` if the left- and right-hand side `u` and `v` are (definitionally) equal. This rule results in a failure if --without-K is enabled (see "Pattern Matching Without K" by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014). - *Solution* solves an equation if one side is (eta-equivalent to) a flexible variable. In case both sides are flexible variables, the unification strategy makes a choice according to the `chooseFlex` function in `Agda.TypeChecking.Rules.LHS.Problem`. - *Injectivity* decomposes an equation of the form `c us =?= c vs : D pars is` where `c : Δc → D pars js` is a constructor of the inductive datatype `D` into a sequence of equations `us =?= vs : delta`. In case `D` is an indexed datatype, *higher-dimensional unification* is applied (see below). - *Conflict* detects absurd equations of the form `c₁ us =?= c₂ vs : D pars is` where `c₁` and `c₂` are two distinct constructors of the datatype `D`. - *Cycle* detects absurd equations of the form `x =?= v : D pars is` where `x` is a variable of the datatype `D` that occurs strongly rigid in `v`. - *EtaExpandVar* eta-expands a single flexible variable `x : R` where `R` is a (eta-expandable) record type, replacing it by one variable for each field of `R`. - *EtaExpandEquation* eta-expands an equation `u =?= v : R` where `R` is a (eta-expandable) record type, replacing it by one equation for each field of `R`. The left- and right-hand sides of these equations are the projections of `u` and `v`. - *LitConflict* detects absurd equations of the form `l₁ =?= l₂ : A` where `l₁` and `l₂` are distinct literal terms. - *StripSizeSuc* simplifies an equation of the form `sizeSuc x =?= sizeSuc y : Size` to `x =?= y : Size`. - *SkipIrrelevantEquation`removes an equation between irrelevant terms. - *TypeConInjectivity* decomposes an equation of the form` D us =?= D vs : Set i`where` D@ is a datatype. This rule is only used if --injective-type-constructors is enabled.

Higher-dimensional unification (new, does not yet appear in any paper): If an equation of the form `c us =?= c vs : D pars is` is encountered where `c : Δc → D pars js` is a constructor of an indexed datatype `D pars : Φ → Set ℓ`, it is in general unsound to just simplify this equation to `us =?= vs : Δc`. For this reason, the injectivity rule in the paper restricts the indices `is` to be distinct variables that are bound in the telescope `eqTel`. But we can be more general by introducing new variables `ks` to the telescope `eqTel` and equating these to `is`: `Δ₁(x : D pars is)Δ₂ ≃ Δ₁(ks : Φ)(x : D pars ks)(ps : is ≡Φ ks)Δ₂` Since `ks` are distinct variables, it's now possible to apply injectivity to the equation `x`, resulting in the following new equation telescope: `Δ₁(ys : Δc)(ps : is ≡Φ js[Δc ↦ ys])Δ₂` Now we can solve the equations `ps` by recursively calling the unification algorithm with flexible variables `Δ₁(ys : Δc)`. This is called *higher-dimensional unification* since we are unifying equality proofs rather than terms. If the higher-dimensional unification succeeds, the resulting telescope serves as the new equation telescope for the original unification problem.

Synopsis

- type UnificationResult = UnificationResult' (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern])
- data UnificationResult' a
  - = Unifies a
  - | NoUnify NegativeUnification
  - | DontKnow [UnificationFailure]
- unifyIndices :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult

# Documentation

type UnificationResult = UnificationResult' (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern]) Source #

Result of `unifyIndices`.

data UnificationResult' a Source #

Constructors

Unifies a | Unification succeeded.
NoUnify NegativeUnification | Terms are not unifiable.
DontKnow [UnificationFailure] | Some other error happened, unification got stuck.

Instances

Functor UnificationResult' Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify Methods fmap :: (a -> b) -> UnificationResult' a -> UnificationResult' b Source # (<$) :: a -> UnificationResult' b -> UnificationResult' a Source #
Foldable UnificationResult' Source # |

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify

Methods

fold :: Monoid m => UnificationResult' m -> m Source #

foldMap :: Monoid m => (a -> m) -> UnificationResult' a -> m Source #

foldr :: (a -> b -> b) -> b -> UnificationResult' a -> b Source #

foldr' :: (a -> b -> b) -> b -> UnificationResult' a -> b Source #

foldl :: (b -> a -> b) -> b -> UnificationResult' a -> b Source #

foldl' :: (b -> a -> b) -> b -> UnificationResult' a -> b Source #

foldr1 :: (a -> a -> a) -> UnificationResult' a -> a Source #

foldl1 :: (a -> a -> a) -> UnificationResult' a -> a Source #

toList :: UnificationResult' a -> [a] Source #

null :: UnificationResult' a -> Bool Source #

length :: UnificationResult' a -> Int Source #

elem :: Eq a => a -> UnificationResult' a -> Bool Source #

maximum :: Ord a => UnificationResult' a -> a Source #

minimum :: Ord a => UnificationResult' a -> a Source #

sum :: Num a => UnificationResult' a -> a Source #

product :: Num a => UnificationResult' a -> a Source #

Traversable UnificationResult' Source # |

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify

Methods

traverse :: Applicative f => (a -> f b) -> UnificationResult' a -> f (UnificationResult' b) Source #

sequenceA :: Applicative f => UnificationResult' (f a) -> f (UnificationResult' a) Source #

mapM :: Monad m => (a -> m b) -> UnificationResult' a -> m (UnificationResult' b) Source #

sequence :: Monad m => UnificationResult' (m a) -> m (UnificationResult' a) Source #

Show a => Show (UnificationResult' a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify Methods showsPrec :: Int -> UnificationResult' a -> ShowS Source # show :: UnificationResult' a -> String Source # showList :: [UnificationResult' a] -> ShowS Source #

unifyIndices :: MonadTCM tcm => Telescope -> FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult Source #

Unify indices.

In `unifyIndices gamma flex us vs`,

`us` and `vs` are the argument lists to unify,

`gamma` is the telescope of free variables in `us` and `vs`.

`flex` is the set of flexible (instantiable) variabes in `us` and `vs`.

The result is the most general unifier of `us` and `vs`.