Safe Haskell | None |
---|---|
Language | Haskell98 |
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
-symbol f (postulate, function, data, record, constructor).
Further, Def
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.
- requireOptionRewriting :: TCM ()
- verifyBuiltinRewrite :: Term -> Type -> TCM ()
- data RelView = RelView {}
- relView :: Type -> TCM (Maybe RelView)
- addRewriteRule :: QName -> TCM ()
- addRewriteRules :: QName -> RewriteRules -> TCM ()
- rewriteWith :: Maybe Type -> Term -> RewriteRule -> ReduceM (Either (Blocked Term) Term)
- rewrite :: Blocked Term -> ReduceM (Either (Blocked Term) Term)
- class NLPatVars a where
- rewArity :: RewriteRule -> Int
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 rhs : A) → Set ℓ
.
Note: we do not care about hiding/non-hiding of lhs and rhs.
Deconstructing a type into Δ → t → t' → core
.
RelView | |
|
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
rewArity :: RewriteRule -> Int Source