Agda.TypeChecking.Rewriting

Rewriting with arbitrary rules.

The user specifies a relation symbol by the pragma {--} where rel should be of type Δ → (lhs rhs : A) → Set i.

Then the user can add rewrite rules by the pragma {--} where q should be a closed term of type Γ → rel us lhs rhs.

We then intend to add a rewrite rule Γ ⊢ lhs ↦ rhs : B to the signature where B = A[us/Δ].

To this end, we normalize lhs, which should be of the form f ts for a Def-symbol f (postulate, function, data, record, constructor). Further, FV(ts) = dom(Γ). The rule q :: Γ ⊢ f ts ↦ rhs : B is added to the signature to the definition of f.

When reducing a term Ψ ⊢ f vs is stuck, we try the rewrites for f, by trying to unify vs with ts. This is for now done by substituting fresh metas Xs for the bound variables in ts and checking equality with vs Ψ ⊢ (f ts)[XsΓ] = f vs : B[XsΓ] If successful (no open metas/constraints), we replace f vs by rhs[Xs/Γ] and continue reducing.

Documentation

requireOptionRewriting :: TCM ()

verifyBuiltinRewrite :: Term -> Type -> TCM ()

Check that the name given to the BUILTIN REWRITE is actually a relation symbol. I.e., its type should be of the form Δ → (lhs : A) (rhs : B) → Set ℓ. Note: we do not care about hiding/non-hiding of lhs and rhs.

data RelView

Deconstructing a type into Δ → t → t' → core.

Constructors

RelView

Fields

• relViewTel :: Telescope

  The whole telescope Δ, t, t'.

• relViewDelta :: ListTel

  Δ.

• relViewType :: Dom Type

  t.

• relViewType' :: Dom Type

  t'.

• relViewCore :: Type

  core.

relView :: Type -> TCM (Maybe RelView)

Deconstructing a type into Δ → t → t' → core. Returns Nothing if not enough argument types.

addRewriteRule :: QName -> TCM ()

Add q : Γ → rel us lhs rhs as rewrite rule Γ ⊢ lhs ↦ rhs : B to the signature where B = A[us/Δ]. Remember that rel : Δ → A → A → Set i, so rel us : (lhs rhs : A[us/Δ]) → Set i.

addRewriteRules :: QName -> RewriteRules -> TCM ()

Append rewrite rules to a definition.

rewriteWith :: Maybe Type -> Term -> RewriteRule -> Elims -> ReduceM (Either (Blocked Term) Term)

rewriteWith t f es rew tries to rewrite f es : t with rew, returning the reduct if successful.

rewrite :: Blocked_ -> Term -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)

rewrite b v rules es tries to rewrite v applied to es with the rewrite rules rules. b is the default blocking tag.

Auxiliary functions

class NLPatVars a where

Minimal complete definition

nlPatVarsUnder

Methods

nlPatVarsUnder :: Int -> a -> IntSet

nlPatVars :: a -> IntSet

Instances

NLPatVars NLPType

Methods

nlPatVarsUnder :: Int -> NLPType -> IntSet

nlPatVars :: NLPType -> IntSet

NLPatVars NLPat

Methods

nlPatVarsUnder :: Int -> NLPat -> IntSet

nlPatVars :: NLPat -> IntSet

(Foldable f, NLPatVars a) => NLPatVars (f a)

Methods

nlPatVarsUnder :: Int -> f a -> IntSet

nlPatVars :: f a -> IntSet

rewArity :: RewriteRule -> Int

class GetMatchables a where

Get all symbols that a rewrite rule matches against

Minimal complete definition

getMatchables

Methods

getMatchables :: a -> [QName]

Instances

GetMatchables RewriteRule

Methods

getMatchables :: RewriteRule -> [QName]

GetMatchables NLPat

Methods

getMatchables :: NLPat -> [QName]

(Foldable f, GetMatchables a) => GetMatchables (f a)

Methods

getMatchables :: f a -> [QName]

Orphan instances

Free NLPType

Methods

freeVars' :: IsVarSet c => NLPType -> FreeM c

Free NLPat

Methods

freeVars' :: IsVarSet c => NLPat -> FreeM c