Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Factor rewriter reification through Ltac2 Constr.Usafe.iter #111

Merged
merged 1 commit into from
Sep 19, 2023
Merged

Factor rewriter reification through Ltac2 Constr.Usafe.iter #111

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 2 additions & 12 deletions src/Rewriter/Rewriter/Reify.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -378,10 +378,7 @@ Module Compilers.
Control.refine (fun () => 'I)) in
() in
match Constr.Unsafe.kind fv with
| Constr.Unsafe.Rel _ => () | Constr.Unsafe.Meta _ => () | Constr.Unsafe.Sort _ => () | Constr.Unsafe.Constant _ _ => () | Constr.Unsafe.Ind _ _ => ()
| Constr.Unsafe.Constructor _ _ => () | Constr.Unsafe.Uint63 _ => () | Constr.Unsafe.Float _ => ()
| Constr.Unsafe.Var v => check_var v None (fun () => ())
| Constr.Unsafe.Cast c _ t => aux c; aux t
| Constr.Unsafe.Prod b c
=> under [b] (fun ns => aux (subst_ns ns c))
| Constr.Unsafe.Lambda b c
Expand All @@ -396,14 +393,6 @@ Module Compilers.
=> check_var v (Some l) default
| _ => default ()
end
| Constr.Unsafe.Case _ x iv y bl
=> Array.iter aux bl;
Constr.Unsafe.Case.iter_invert aux iv;
aux x;
aux y
| Constr.Unsafe.Proj _p c => aux c
| Constr.Unsafe.Array _u t def ty =>
Array.iter aux t; aux def; aux ty
| Constr.Unsafe.Fix _ _ tl bl =>
under (Array.to_list tl)
(fun ns => let subst_ns := subst_ns ns in
Expand All @@ -412,7 +401,8 @@ Module Compilers.
under (Array.to_list tl)
(fun ns => let subst_ns := subst_ns ns in
Array.iter (fun c => aux (subst_ns c)) bl)
| Constr.Unsafe.Evar _ l => () (* not possible to iter in Ltac2... *)
| _ => (* TODO: factor binder logic through something like [Constr.Unsafe.iter_with_full_binders] *)
Constr.Unsafe.iter aux fv
end) in
aux fv;
match res.(contents) with
Expand Down
29 changes: 29 additions & 0 deletions src/Rewriter/Util/Tactics2/Constr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,35 @@ Module Unsafe.
end.
End Case.

(** [iter f c] iters [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
Ltac2 iter (f : constr -> unit) (c : constr) : unit :=
match kind c with
| Rel _ => () | Meta _ => () | Var _ => () | Sort _ => () | Constant _ _ => () | Ind _ _ => ()
| Constructor _ _ => () | Uint63 _ => () | Float _ => ()
| Cast c _ t => f c; f t
| Prod b c => f (Binder.type b); f c
| Lambda b c => f (Binder.type b); f c
| LetIn b t c => f (Binder.type b); f t; f c
| App c l => f c; Array.iter f l
| Evar _ l => () (* not possible to iter in Ltac2... *)
| Case _ x iv y bl
=> Array.iter f bl;
Case.iter_invert f iv;
f x;
f y
| Proj _p c => f c
| Fix _ _ tl bl =>
Array.iter (fun b => f (Binder.type b)) tl;
Array.iter f bl
| CoFix _ tl bl =>
Array.iter (fun b => f (Binder.type b)) tl;
Array.iter f bl
| Array _u t def ty =>
Array.iter f t; f def; f ty
end.

(** [iter_with_binders g f n c] iters [f n] on the immediate
subterms of [c]; it carries an extra data [n] (typically a lift
index) which is processed by [g] (which typically add 1 to [n]) at
Expand Down
Loading