Agda-2.4.2.3: 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

Turn a term into a non-linear pattern, treating the free variables as pattern variables.

Methods

patternFrom :: a -> TCM b

Instances

type NLM = MaybeT (WriterT NLMOut ReduceM)

Monad for non-linear matching.

liftRed :: ReduceM a -> NLM a

traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a

tellSubst :: Int -> Term -> NLM ()

Add substitution i |-> v to result of matching.

tellEq :: Term -> Term -> NLM ()

newtype AmbSubst

Non-linear matching returns first an ambiguous substitution, mapping one de Bruijn index to possibly several terms.

Constructors

AmbSubst 

Fields

ambSubst :: IntMap [Term]
 

data PostponedEquation

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

Constructors

PostponedEquation 

Fields

eqLhs :: Term

Term from pattern, living in pattern context.

eqRhs :: Term

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

class AmbMatch a b where

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

Methods

ambMatch :: a -> b -> NLM ()

Instances

AmbMatch NLPat Term 
AmbMatch a b => AmbMatch [a] [b] 
AmbMatch a b => AmbMatch (Elim' a) (Elim' b) 
AmbMatch a b => AmbMatch (Arg a) (Arg b) 

equal :: Term -> Term -> ReduceM Bool

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