Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.
Synopsis
- 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 -> Elims -> ReduceM (Either (Blocked Term) Term)
- rewrite :: Blocked_ -> Term -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)
- class NLPatVars a where
- rewArity :: RewriteRule -> Int
- class GetMatchables a where
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
.
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 :: Maybe Type -> Term -> RewriteRule -> Elims -> ReduceM (Either (Blocked Term) Term) Source #
rewriteWith t f es rew
tries to rewrite f es : t
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 # |