Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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.



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

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

data RelView Source

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




relViewTel :: Telescope

The whole telescope Δ, t, t'.

relViewDelta :: ListTel


relViewType :: Type


relViewType' :: Type


relViewCore :: Type


relView :: Type -> TCM (Maybe RelView) Source

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

addRewriteRule :: QName -> TCM () Source

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.

Makes only sense in empty context.

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

Append rewrite rules to a definition.

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

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

rewrite :: Blocked Term -> ReduceM (Either (Blocked Term) Term) Source

rewrite t tries to rewrite a reduced term.

Auxiliary functions

class NLPatVars a where Source


nlPatVars :: a -> IntSet Source