Commit 199d205a authored by Robbert Krebbers's avatar Robbert Krebbers

Fix #184.

parent e53c497d
Pipeline #8313 passed with stage
in 11 minutes and 44 seconds
...@@ -351,10 +351,11 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit := ...@@ -351,10 +351,11 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
end. end.
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
match v1, v2 with match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2 | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
| LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2 | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
| v1, v2 => guard (op = EqOp); Some $ LitV $ LitBool $ bool_decide (v1 = v2) | _, _ => None
end. end.
Inductive head_step : expr state expr state list (expr) Prop := Inductive head_step : expr state expr state list (expr) Prop :=
......
...@@ -71,6 +71,11 @@ Section LiftingTests. ...@@ -71,6 +71,11 @@ Section LiftingTests.
wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done. wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
Qed. Qed.
Definition heap_e6 : val := λ: "v", "v" = "v".
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, w = #true }})%I.
Proof. wp_lam. wp_op. by case_bool_decide. Qed.
Definition FindPred : val := Definition FindPred : val :=
rec: "pred" "x" "y" := rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in let: "yp" := "y" + #1 in
......
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