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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Rewriting.NonLinMatch

Description

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

Documentation

class PatternFrom a b where Source

Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument is the number of bound variables (from pattern lambdas).

Methods

patternFrom :: Int -> a -> TCM b Source

type NLM = ExceptT Blocked_ (StateT NLMState ReduceM) Source

Monad for non-linear matching.

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

Constructors

PostponedEquation 

Fields

eqFreeVars :: Telescope

Telescope of free variables in the equation

eqLhs :: Term

Term from pattern, living in pattern context.

eqRhs :: Term

Term from scrutinee, living in context where matching was invoked.

Instances

class Match a b where Source

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

Methods

match Source

Arguments

:: Telescope

The telescope of pattern variables

-> Telescope

The telescope of lambda-bound variables

-> a

The pattern to match

-> b

The term to be matched against the pattern

-> NLM () 

Instances

Match NLPat Term Source 
Match a b => Match [a] [b] Source 
Match a b => Match (Dom a) (Dom b) Source 
Match a b => Match (Arg a) (Arg b) Source 
Match a b => Match (Type' a) (Type' b) Source 
(Match a b, Subst t1 a, Subst t2 b) => Match (Abs a) (Abs b) Source 
Match a b => Match (Elim' a) (Elim' b) Source 

equal :: Term -> Term -> ReduceM Bool Source

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

class RaiseNLP a where Source

Raise (bound) variables in a NLPat

Minimal complete definition

raiseNLPFrom

Methods

raiseNLPFrom :: Int -> Int -> a -> a Source

raiseNLP :: Int -> a -> a Source