Commit bd4b5d0a authored by Michael Sammler's avatar Michael Sammler
Browse files

update iris version and fix warnings

parent d671905b
Pipeline #33509 passed with stage
in 19 minutes and 46 seconds
......@@ -14,7 +14,7 @@ RefinedC: Framework for verifying low-level code using refinement types and owne
depends: [
"coq" { (>= "8.11.0" & < "8.12~") | (= "dev") }
"coq-iris" { (= "dev.2020-07-24.0.9b804e35") | (= "dev") }
"coq-iris" { (= "dev.2020-09-03.1.7dd1b9af") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -289,6 +289,6 @@ Ltac enrich_context_tac ::=
repeat match goal with
| |- context C [ rotate_nat_add ?s ?o ?e ] =>
let G := context C[enrich_marker rotate_nat_add s o e] in
convert_concl_no_check G;
change_no_check G;
try have ?:=rotate_nat_add_lt s o e ltac:(lia)
end.
......@@ -255,7 +255,7 @@ Tactic Notation "liEnforceInvariant" :=
end
end in
with_H ltac:(fun H =>
convert_concl_no_check (envs_entails H P)
change_no_check (envs_entails H P)
)
end.
Ltac liFresh :=
......@@ -269,7 +269,7 @@ Ltac liFresh :=
let H2 := fresh "IPM_INTERNAL" in
pose (H2 := @Envs PROP p1 p2 c');
change (envs PROP) with (@IPM_STATE PROP c') in H2;
convert_concl_no_check (@envs_entails PROP H2 Q);
change_no_check (@envs_entails PROP H2 Q);
clear H; rename H2 into H
end
end in
......@@ -550,7 +550,7 @@ Ltac record_destruct_hint hint info := idtac.
Ltac liDestructHint :=
lazymatch goal with
| |- @envs_entails ?PROP ?Δ (destruct_hint ?hint ?info ?T) =>
convert_concl_no_check (@envs_entails PROP Δ T);
change_no_check (@envs_entails PROP Δ T);
lazymatch hint with
| DHintInfo =>
record_destruct_hint hint info
......
......@@ -80,15 +80,15 @@ Ltac liRIntroduceLetInGoal :=
let H := fresh "GOAL" in
lazymatch P with
| @bi_wand ?PROP ?Q ?T =>
pose H := (LET_ID T); convert_concl_no_check (@envs_entails PROP Δ (@bi_wand PROP Q H))
pose H := (LET_ID T); change_no_check (@envs_entails PROP Δ (@bi_wand PROP Q H))
| @typed_val_expr ?Σ ?tG ?e ?T =>
pose (H := LET_ID T); convert_concl_no_check (@envs_entails PROP Δ (@typed_val_expr Σ tG e H))
pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_val_expr Σ tG e H))
| @typed_write ?Σ ?tG ?b ?e ?v ?ty ?Mov ?T =>
pose (H := LET_ID T); convert_concl_no_check (@envs_entails PROP Δ (@typed_write Σ tG b e v ty Mov H))
pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_write Σ tG b e v ty Mov H))
| @typed_place ?Σ ?tG ?P ?l1 ?β1 ?ty1 ?T =>
pose (H := LET_ID T); convert_concl_no_check (@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H))
pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H))
| @typed_bin_op ?Σ ?tG ?v1 ?P1 ?v2 ?P2 ?op ?ot1 ?ot2 ?T =>
pose (H := LET_ID T); convert_concl_no_check (@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H))
pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H))
end
end.
......@@ -112,7 +112,7 @@ Ltac liRStmt :=
lazymatch s with
| LocInfo ?info ?s2 =>
update_loc_info (Some info);
convert_concl_no_check (envs_entails Δ (typed_stmt s2 fn ls fr Q))
change_no_check (envs_entails Δ (typed_stmt s2 fn ls fr Q))
| _ => update_loc_info (None : option location_info)
end
end;
......@@ -153,7 +153,7 @@ Ltac liRPopLocationInfo :=
(* TODO: don't hardcode this for two arguments *)
| |- envs_entails ?Δ (pop_location_info ?info ?T ?a1 ?a2) =>
update_loc_info [info; info];
convert_concl_no_check (envs_entails Δ (T a1 a2))
change_no_check (envs_entails Δ (T a1 a2))
end.
Ltac liRExpr :=
......@@ -162,7 +162,7 @@ Ltac liRExpr :=
lazymatch e with
| LocInfo ?info ?e2 =>
update_loc_info [info];
convert_concl_no_check (envs_entails Δ (typed_val_expr e2 (pop_location_info info T)))
change_no_check (envs_entails Δ (typed_val_expr e2 (pop_location_info info T)))
| _ => idtac
end
end;
......@@ -242,7 +242,7 @@ Ltac split_blocks Pfull Ps :=
let Q := fresh "Q" in
lazymatch goal with
| |- @envs_entails ?PROP ?Δ (@bi_wand _ ?P (@typed_stmt ?Σ ?tG ?B ?s ?fn ?ls ?fr ?Q')) =>
pose (Q := (Q')); convert_concl_no_check (@envs_entails PROP Δ (@bi_wand PROP P (@typed_stmt Σ tG B s fn ls fr Q)))
pose (Q := (Q')); change_no_check (@envs_entails PROP Δ (@bi_wand PROP P (@typed_stmt Σ tG B s fn ls fr Q)))
end;
let rec pose_Ps Ps :=
lazymatch Ps with
......
......@@ -114,6 +114,6 @@ Hint Extern 5 (Normalize _ (length (replicate _ _)) _) => class_apply normalize_
Ltac normalize_tc :=
first [
lazymatch goal with
| |- ?a = ?b => convert_concl_no_check (NormalizeWalk true a b); solve [refine _]
| |- ?a = ?b => change_no_check (NormalizeWalk true a b); solve [refine _]
end
| exact: eq_refl].
......@@ -119,8 +119,8 @@ Ltac compute_map_lookup :=
solve [repeat lazymatch goal with
| |- <[?x:=?s]> ?Q !! ?y = Some ?res =>
lazymatch x with
| y => convert_concl_no_check (Some s = Some res); reflexivity
| _ => convert_concl_no_check (Q !! y = Some res)
| y => change_no_check (Some s = Some res); reflexivity
| _ => change_no_check (Q !! y = Some res)
end
end ].
......@@ -130,20 +130,20 @@ Ltac enrich_context_base :=
repeat match goal with
| |- context C [ ?a `quot` ?b ] =>
let G := context C[enrich_marker Z.quot a b] in
convert_concl_no_check G;
change_no_check G;
try have ?:=Z.quot_lt a b ltac:(lia) ltac:(lia);
try have ?:=Z.quot_pos a b ltac:(lia) ltac:(lia)
| |- context C [ ?a `rem` ?b ] =>
let G := context C[enrich_marker Z.rem a b] in
convert_concl_no_check G;
change_no_check G;
try have ?:=Z.rem_bound_pos a b ltac:(lia) ltac:(lia)
| |- context C [ ?a `mod` ?b ] =>
let G := context C[enrich_marker Z.modulo a b] in
convert_concl_no_check G;
change_no_check G;
try have ?:=Z.mod_bound_pos a b ltac:(lia) ltac:(lia)
| |- context C [ length (filter ?P ?l) ] =>
let G := context C[enrich_marker length (filter P l)] in
convert_concl_no_check G;
change_no_check G;
pose proof (filter_length P l)
end.
......
......@@ -86,7 +86,7 @@ Ltac normalize3 :=
notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _);
[normalize3|normalize3|
lazymatch goal with
| |- ?A = ?B => convert_concl_no_check (Normalize A B)
| |- ?A = ?B => change_no_check (Normalize A B)
end; solve [ refine _ ] ]) ||
exact: eq_refl
| _ => exact: eq_refl
......@@ -124,7 +124,7 @@ Ltac normalize4 :=
go actx a;
refine (eq_ind_r ctx _ _);[|
lazymatch goal with
| |- ?A = ?B => convert_concl_no_check (Normalize A B)
| |- ?A = ?B => change_no_check (Normalize A B)
end; solve [ refine _ ]
]
......@@ -133,7 +133,7 @@ Ltac normalize4 :=
(* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _); *)
(* [normalize3|normalize3| *)
(* lazymatch goal with *)
(* | |- ?A = ?B => convert_concl_no_check (Normalize A B) *)
(* | |- ?A = ?B => change_no_check (Normalize A B) *)
(* end; solve [ refine _ ] ]) || *)
(* exact: eq_refl *)
| _ => idtac
......@@ -183,7 +183,7 @@ Goal ∀ l i (x : Z),
(* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _); *)
(* [normalize3|normalize3| *)
(* lazymatch goal with *)
(* | |- ?A = ?B => convert_concl_no_check (Normalize true A B) *)
(* | |- ?A = ?B => change_no_check (Normalize true A B) *)
(* end; solve [ refine _ ] ]. *)
......@@ -219,7 +219,7 @@ Goal ∀ l i (x : Z),
(* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _); *)
(* [normalize3|normalize3| *)
(* lazymatch goal with *)
(* | |- ?A = ?B => convert_concl_no_check (Normalize A B) *)
(* | |- ?A = ?B => change_no_check (Normalize A B) *)
(* end; solve [ refine _ ] ]). *)
(* exact: eq_refl. *)
......@@ -227,7 +227,7 @@ Goal ∀ l i (x : Z),
(* notypeclasses refine (tac_f_equal_fn2 _ _ _ _ _ _ _ _ _); *)
(* [normalize3|normalize3| *)
(* lazymatch goal with *)
(* | |- ?A = ?B => convert_concl_no_check (Normalize A B) *)
(* | |- ?A = ?B => change_no_check (Normalize A B) *)
(* end; solve [ refine _ ] | ]. *)
......@@ -235,7 +235,7 @@ Goal ∀ l i (x : Z),
(* notypeclasses refine (tac_eq_replace _ _ _ _). *)
(* notypeclasses refine (tac_f_equal_fn _ _ _ _ _ _ _ _). exact: eq_refl. exact: eq_refl. *)
(* lazymatch goal with *)
(* | |- ?A = ?B => convert_concl_no_check (Normalize A B) *)
(* | |- ?A = ?B => change_no_check (Normalize A B) *)
(* end. *)
......
......@@ -277,7 +277,7 @@ Ltac solve_into_place_ctx :=
match goal with
| |- IntoPlaceCtx ?e ?T =>
let e' := W.of_expr e in
convert_concl_no_check (IntoPlaceCtx (W.to_expr e') T);
change_no_check (IntoPlaceCtx (W.to_expr e') T);
refine (find_place_ctx_correct _ _ _); rewrite/=/W.to_expr/=; done
end.
Hint Extern 0 (IntoPlaceCtx _ _) => solve_into_place_ctx : typeclass_instances.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment