Safe Haskell | None |
---|---|

Language | Haskell2010 |

Non-linear matching of the lhs of a rewrite rule against a neutral term.

Given a lhs

Δ ⊢ lhs : B

and a candidate term

Γ ⊢ t : A

we seek a substitution Γ ⊢ σ : Δ such that

Γ ⊢ B[σ] = A and Γ ⊢ lhs[σ] = t : A

## Synopsis

- class PatternFrom t a b where
- patternFrom :: Relevance -> Int -> t -> a -> TCM b

- type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)
- data NLMState = NLMState {}
- nlmSub :: Lens' Sub NLMState
- nlmEqs :: Lens' PostponedEquations NLMState
- runNLM :: MonadReduce m => NLM () -> m (Either Blocked_ NLMState)
- matchingBlocked :: Blocked_ -> NLM ()
- tellSub :: Relevance -> Int -> Term -> NLM ()
- tellEq :: Telescope -> Telescope -> Term -> Term -> NLM ()
- type Sub = IntMap (Relevance, Term)
- data PostponedEquation = PostponedEquation {}
- type PostponedEquations = [PostponedEquation]
- class Match t a b where
- reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a))
- makeSubstitution :: Telescope -> Sub -> Substitution
- checkPostponedEquations :: (MonadReduce m, HasConstInfo m, MonadDebug m) => Substitution -> PostponedEquations -> m (Maybe Blocked_)
- nonLinMatch :: (MonadReduce m, HasConstInfo m, MonadDebug m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
- equal :: (MonadReduce m, HasConstInfo m) => Term -> Term -> m (Maybe Blocked_)

# Documentation

class PatternFrom t a b where Source #

Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument indicates the relevance we are working under: if this is Irrelevant, then we construct a pattern that never fails to match. The second argument is the number of bound variables (from pattern lambdas). The third argument is the type of the term.

## Instances

PatternFrom () Sort NLPat Source # | |

Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |

PatternFrom () Type NLPType Source # | |

Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |

PatternFrom Type Term NLPat Source # | |

Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |

PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source # | |

Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |

PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # | |

Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |

PatternFrom (Type, Term) Elims [Elim' NLPat] Source # | |

matchingBlocked :: Blocked_ -> NLM () Source #

tellSub :: Relevance -> Int -> Term -> NLM () Source #

Add substitution `i |-> v`

to result of matching.

data PostponedEquation Source #

Matching against a term produces a constraint which we have to verify after applying the substitution computed by matching.

type PostponedEquations = [PostponedEquation] Source #

class Match t a b where Source #

Match a non-linear pattern against a neutral term, returning a substitution.

reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a)) Source #

makeSubstitution :: Telescope -> Sub -> Substitution Source #

checkPostponedEquations :: (MonadReduce m, HasConstInfo m, MonadDebug m) => Substitution -> PostponedEquations -> m (Maybe Blocked_) Source #

nonLinMatch :: (MonadReduce m, HasConstInfo m, MonadDebug m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution) Source #

equal :: (MonadReduce m, HasConstInfo m) => Term -> Term -> m (Maybe Blocked_) Source #

Untyped βη-equality, does not handle things like empty record types.
Returns `Nothing`

if the terms are equal, or `Just b` if the terms are not
(where b contains information about possible metas blocking the comparison)