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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rewriting

Description

Rewriting with arbitrary rules.

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

Then the user can add rewrite rules by the pragma `{-# REWRITE q #-}` 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.

Synopsis

- requireOptionRewriting :: TCM ()
- verifyBuiltinRewrite :: Term -> Type -> TCM ()
- data RelView = RelView {
  - relViewTel :: Telescope
  - relViewDelta :: ListTel
  - relViewType :: Dom Type
  - relViewType' :: Dom Type
  - relViewCore :: Type
  }
- relView :: Type -> TCM (Maybe RelView)
- addRewriteRules :: [QName] -> TCM ()
- rewriteRelationDom :: QName -> TCM (ListTel, Dom Type)
- checkRewriteRule :: QName -> TCM (Maybe RewriteRule)
- rewriteWith :: Type -> (Elims -> Term) -> RewriteRule -> Elims -> ReduceM (Either (Blocked Term) Term)
- rewrite :: Blocked_ -> (Elims -> Term) -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)

# Documentation

requireOptionRewriting :: TCM () Source #

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 : A) (rhs : B) → Set ℓ`. Note: we do not care about hiding/non-hiding of lhs and rhs.

data RelView Source #

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) Source #

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

addRewriteRules :: [QName] -> TCM () Source #

Check the given rewrite rules and add them to the signature.

rewriteRelationDom :: QName -> TCM (ListTel, Dom Type) Source #

Get domain of rewrite relation.

checkRewriteRule :: QName -> TCM (Maybe RewriteRule) Source #

Check the validity of `q : Γ → rel us lhs rhs` as rewrite rule `Γ ⊢ lhs ↦ rhs : B` where `B = A[us/Δ]`. Remember that `rel : Δ → A → A → Set i`, so `rel us : (lhs rhs : A[us/Δ]) → Set i`. Returns the checked rewrite rule to be added to the signature.

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

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

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

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