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

Adapt to coq/coq#18280 (case relevance outside case info) #122

Merged
merged 1 commit into from
Nov 13, 2023
Merged

Adapt to coq/coq#18280 (case relevance outside case info) #122

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
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,7 @@ src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib

src/Rewriter/Util/Tactics2/Constr.v
src/Rewriter/Util/Tactics2/DestCase.v
src/Rewriter/Util/Tactics2/DestProj.v
src/Rewriter/Util/Tactics2/Proj.v

Expand Down
1 change: 1 addition & 0 deletions Makefile.local.common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ COMPATIBILITY_FILES := \
src/Rewriter/Util/plugins/StrategyTactic.v \
src/Rewriter/Util/plugins/Ltac2Extra.v \
src/Rewriter/Util/Tactics2/Constr.v \
src/Rewriter/Util/Tactics2/DestCase.v \
src/Rewriter/Util/Tactics2/DestProj.v \
src/Rewriter/Util/Tactics2/Proj.v \
#
4 changes: 3 additions & 1 deletion src/Rewriter/Language/Reify.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
Require Rewriter.Util.Tactics2.String.
Require Rewriter.Util.Tactics2.Constr.
Require Import Rewriter.Util.Tactics2.DestEvar.
Require Import Rewriter.Util.Tactics2.DestCase.
Require Import Rewriter.Util.Tactics2.InstantiateEvar.
Require Import Rewriter.Util.Tactics2.Constr.Unsafe.MakeAbbreviations.
Require Import Rewriter.Util.Tactics2.FixNotationsForPerformance.
Expand Down Expand Up @@ -63,8 +64,8 @@
f c.
Ltac2 reified_of_constr (c : constr) : ident
:= Ident.of_constr refine_constant_to_lambda_reified c.
End Ident.

Check warning on line 67 in src/Rewriter/Language/Reify.v

View workflow job for this annotation

GitHub Actions / build-docker (8.16) 

Trying to mask the absolute name "Ltac2.Ident"!
End Ltac2.

Check warning on line 68 in src/Rewriter/Language/Reify.v

View workflow job for this annotation

GitHub Actions / build-docker (8.16) 

Trying to mask the absolute name "Ltac2.Ident"!

(* this is very super-linear, should not be used in production code *)
Ltac2 with_term_in_context (cache : (unit -> binder) list) (tys : constr list) (term : constr) (tac : constr -> unit) : unit :=
Expand Down Expand Up @@ -306,7 +307,7 @@
#[deprecated(since="8.15",note="Use Ltac2 type.reify instead.")]
Ltac reify base_reify base_type ty :=
let f := ltac2:(base_reify base_type ty
|- Control.refine (fun () => reify (fun v => Ltac1.apply_c base_reify [v]) (Ltac1.get_to_constr "type.reify:base_type" base_type) (Ltac1.get_to_constr "type.reify:ty" ty))) in

Check warning on line 310 in src/Rewriter/Language/Reify.v

View workflow job for this annotation

GitHub Actions / build-docker (8.16) 

Ltac2 definition Ltac1.get_to_constr is deprecated since 8.15.
Use Ltac2 instead.
constr:(ltac:(f base_reify base_type ty)).

Class reified_of {base_type} {interp_base_type : base_type -> Type} (v : Type) (rv : type base_type)
Expand Down Expand Up @@ -510,8 +511,9 @@
reify_preprocess v
end
end
| Constr.Unsafe.Case cinfo ret_ty cinv x branches
| Constr.Unsafe.Case _ _ _ _ _
=> Reify.debug_enter_reify_case "expr.reify_preprocess" "Case" term;
let (cinfo, ret_ty, cinv, x, branches) := destCase term in
match Constr.Unsafe.kind ret_ty with
| Constr.Unsafe.Lambda xb ret_ty
=> let ty := Constr.Unsafe.substnl [x] 0 ret_ty in
Expand Down
4 changes: 2 additions & 2 deletions src/Rewriter/Util/Tactics2/Constr.v.v819
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ Module Unsafe.
| Case _ x iv y bl
=> Array.iter f bl;
Case.iter_invert f iv;
f x;
match x with (x,_) => f x end;
JasonGross marked this conversation as resolved.
Show resolved Hide resolved
f y
| Proj _p _ c => f c
| Fix _ _ tl bl =>
Expand Down Expand Up @@ -82,7 +82,7 @@ Module Unsafe.
| Case _ x iv y bl
=> Array.iter (f n) bl;
Case.iter_invert (f n) iv;
f n x;
match x with (x,_) => f n x end;
JasonGross marked this conversation as resolved.
Show resolved Hide resolved
f n y
| Proj _p _ c => f n c
| Fix _ _ tl bl =>
Expand Down
1 change: 1 addition & 0 deletions src/Rewriter/Util/Tactics2/DestCase.v.v815
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
DestCase.v.v818
1 change: 1 addition & 0 deletions src/Rewriter/Util/Tactics2/DestCase.v.v816
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
DestCase.v.v818
1 change: 1 addition & 0 deletions src/Rewriter/Util/Tactics2/DestCase.v.v817
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
DestCase.v.v818
0 src/Rewriter/Util/Tactics2/DestCase.v → src/Rewriter/Util/Tactics2/DestCase.v.v818
View file
Open in desktop
File renamed without changes.
11 changes: 11 additions & 0 deletions src/Rewriter/Util/Tactics2/DestCase.v.v819
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
Require Import Ltac2.Ltac2.
Require Export Rewriter.Util.FixCoqMistakes.
Import Ltac2.Constr.Unsafe.

Ltac2 Type exn ::= [ Not_a_case (kind) ].
Ltac2 destCase (c : constr) :=
let k := kind c in
match k with
| Case a b c d e => let (b,_) := b in (a, b, c, d, e)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more. 

File "./src/Rewriter/Util/Tactics2/DestCase.v", line 9, characters 27-30:
Error: This expression has type constr but an expression was expected of type
'a * 'b

Has the docker image updated yet?

| _ => Control.throw (Not_a_case k)
end.
Loading