Commit dfbfe1bd authored by Ralf Jung's avatar Ralf Jung

bump Iris, fix for array changes

parent 43c04714
Pipeline #17337 passed with stage
in 15 minutes and 37 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-05-24.5.cdb90fa2") | (= "dev") }
"coq-iris" { (= "dev.2019-06-02.0.2c926d86") | (= "dev") }
]
......@@ -376,14 +376,14 @@ Definition dbin_op_eval_bool (op : bin_op) (db1 db2 : dbool) : option dbase_lit
end.
Arguments dbin_op_eval_bool !_ _ _ /.
Definition dbin_op_eval_int (op : bin_op) (di1 di2 : dint) : dbase_lit :=
Definition dbin_op_eval_int (op : bin_op) (di1 di2 : dint) : option dbase_lit :=
match op with
| PlusOp => dLitInt $ dint_plus di1 di2
| MinusOp => dLitInt $ dint_minus di1 di2
| EqOp => dLitBool $ dint_eq di1 di2
| LtOp => dLitBool $ dint_lt di1 di2
| LeOp => dLitBool $ dint_le di1 di2
| _ => dLitUnknown $ bin_op_eval_int op (dint_interp di1) (dint_interp di2)
| PlusOp => Some $ dLitInt $ dint_plus di1 di2
| MinusOp => Some $ dLitInt $ dint_minus di1 di2
| EqOp => Some $ dLitBool $ dint_eq di1 di2
| LtOp => Some $ dLitBool $ dint_lt di1 di2
| LeOp => Some $ dLitBool $ dint_le di1 di2
| _ => dLitUnknown <$> bin_op_eval_int op (dint_interp di1) (dint_interp di2)
(* Do better in case both operands are known *)
end.
Arguments dbin_op_eval_int !_ _ _ /.
......@@ -417,7 +417,7 @@ Arguments dval_eq _ !_ !_ / : simpl nomatch.
Definition dbin_op_eval (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
if decide (op = EqOp) then Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2 else
match dv1, dv2 with
| dLitV (dLitInt di1), dLitV (dLitInt di2) => Some $ dLitV $ dbin_op_eval_int op di1 di2
| dLitV (dLitInt di1), dLitV (dLitInt di2) => dLitV <$> dbin_op_eval_int op di1 di2
| dLitV (dLitBool db1), dLitV (dLitBool db2) => dLitV <$> dbin_op_eval_bool op db1 db2
| _, _ => None
end.
......@@ -568,11 +568,12 @@ Proof.
rewrite H. apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.
Lemma dbin_op_eval_int_correct op di1 di2 :
dbase_lit_interp (dbin_op_eval_int op di1 di2) =
bin_op_eval_int op (dint_interp di1) (dint_interp di2).
Lemma dbin_op_eval_int_correct op di1 di2 dl :
dbin_op_eval_int op di1 di2 = Some dl
bin_op_eval_int op (dint_interp di1) (dint_interp di2) = Some (dbase_lit_interp dl).
Proof.
destruct op; f_equal/=; auto using dint_plus_correct, dint_minus_correct,
destruct op; intros; simplify_eq/=; do 2 f_equal/=;
auto using dint_plus_correct, dint_minus_correct,
dint_eq_correct, dint_lt_correct, dint_le_correct.
Qed.
......@@ -613,7 +614,7 @@ Proof.
rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)); simplify_eq/=.
{ by rewrite dval_eq_correct. }
destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq.
- by rewrite dbin_op_eval_int_correct.
- by erewrite dbin_op_eval_int_correct by done.
- by erewrite dbin_op_eval_bool_correct by done.
Qed.
......
Markdown is supported
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