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

Safe HaskellNone
LanguageHaskell2010

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 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).

Minimal complete definition

patternFrom

Methods

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

Instances
PatternFrom Sort NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

PatternFrom Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

PatternFrom Term NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

PatternFrom a b => PatternFrom [a] [b] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> [a] -> TCM [b] Source #

PatternFrom a b => PatternFrom (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Dom a -> TCM (Dom b) Source #

PatternFrom a b => PatternFrom (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Arg a -> TCM (Arg b) Source #

PatternFrom a b => PatternFrom (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Abs a -> TCM (Abs b) Source #

PatternFrom a NLPat => PatternFrom (Elim' a) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

type NLM = ExceptT Blocked_ (StateT NLMState ReduceM) Source #

Monad for non-linear matching.

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.

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.

class Match a b where Source #

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

Minimal complete definition

match

Methods

match Source #

Arguments

:: Relevance

Are we currently matching in an irrelevant context?

-> 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 NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM () Source #

Match NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Level -> NLM () Source #

Match NLPat Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Sort -> NLM () Source #

Match NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Term -> NLM () Source #

Match a b => Match [a] [b] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> [a] -> [b] -> NLM () Source #

Match a b => Match (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Dom a -> Dom b -> NLM () Source #

Match a b => Match (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Arg a -> Arg b -> NLM () Source #

(Match a b, Subst t1 a, Subst t2 b) => Match (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Abs a -> Abs b -> NLM () Source #

Match a b => Match (Elim' a) (Elim' b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Elim' a -> Elim' b -> NLM () Source #

reallyFree :: (Reduce a, Normalise a, Free a) => (Int -> Bool) -> a -> ReduceM (Either Blocked_ (Maybe a)) Source #

equal :: Term -> Term -> ReduceM (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)

normaliseB' :: (Reduce t, Normalise t) => t -> ReduceM (Blocked t) Source #

Normalise the given term but also preserve blocking tags TODO: implement a more efficient version of this.