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)
 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/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
.
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
rewArity :: RewriteRule > Int Source #
class GetMatchables a where Source #
Get all symbols that a rewrite rule matches against
getMatchables :: a > [QName] Source #
Instances
GetMatchables RewriteRule Source #  
Defined in Agda.TypeChecking.Rewriting getMatchables :: RewriteRule > [QName] Source #  
GetMatchables NLPat Source #  
Defined in Agda.TypeChecking.Rewriting getMatchables :: NLPat > [QName] Source #  
(Foldable f, GetMatchables a) => GetMatchables (f a) Source #  
Defined in Agda.TypeChecking.Rewriting getMatchables :: f a > [QName] Source # 