| 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 DefFV(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 {}
- relView :: Type -> TCM (Maybe RelView)
- addRewriteRules :: [QName] -> TCM ()
- checkRewriteRule :: QName -> TCM RewriteRule
- rewriteWith :: Type -> Term -> RewriteRule -> Elims -> ReduceM (Either (Blocked Term) Term)
- rewrite :: Blocked_ -> 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.
Deconstructing a type into Δ → t → t' → core.
Constructors
| RelView | |
Fields
| |
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.
checkRewriteRule :: QName -> TCM 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.