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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rewriting

Contents

- Auxiliary functions
- Orphan instances

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)
- addRewriteRule :: QName -> TCM ()
- addRewriteRules :: QName -> RewriteRules -> TCM ()
- rewriteWith :: Type -> Term -> RewriteRule -> Elims -> ReduceM (Either (Blocked Term) Term)
- rewrite :: Blocked_ -> Term -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
- class NLPatVars a where
  - nlPatVarsUnder :: Int -> a -> IntSet
  - nlPatVars :: a -> IntSet
- rewArity :: RewriteRule -> Int
- class GetMatchables a where
  - getMatchables :: a -> [QName]

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

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

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

Append rewrite rules to a definition.

rewriteWith :: Type -> 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_ -> 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.

# Auxiliary functions

class NLPatVars a where Source #

Minimal complete definition

nlPatVarsUnder

Methods

nlPatVarsUnder :: Int -> a -> IntSet Source #

nlPatVars :: a -> IntSet Source #

Instances

NLPatVars NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods nlPatVarsUnder :: Int -> NLPType -> IntSet Source # nlPatVars :: NLPType -> IntSet Source #
NLPatVars NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods nlPatVarsUnder :: Int -> NLPat -> IntSet Source # nlPatVars :: NLPat -> IntSet Source #
(Foldable f, NLPatVars a) => NLPatVars (f a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods nlPatVarsUnder :: Int -> f a -> IntSet Source # nlPatVars :: f a -> IntSet Source #

rewArity :: RewriteRule -> Int Source #

class GetMatchables a where Source #

Get all symbols that a rewrite rule matches against

Methods

getMatchables :: a -> [QName] Source #

Instances

GetMatchables RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: RewriteRule -> [QName] Source #
GetMatchables NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: NLPat -> [QName] Source #
(Foldable f, GetMatchables a) => GetMatchables (f a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods getMatchables :: f a -> [QName] Source #

# Orphan instances

Free NLPType Source # |
Instance details Methods freeVars' :: IsVarSet c => NLPType -> FreeM c Source #
Free NLPat Source # |
Instance details Methods freeVars' :: IsVarSet c => NLPat -> FreeM c Source #