Safe Haskell  None 

Language  Haskell2010 
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
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.
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/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.
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.