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/nonhiding 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