Commit 678fdce7 authored by Ralf Jung's avatar Ralf Jung

switch the language over to integers

tests.v is temporarily broken
parent 6a054461
...@@ -32,28 +32,28 @@ Proof. ...@@ -32,28 +32,28 @@ Proof.
by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val. by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val.
Qed. Qed.
Lemma wp_le E (n1 n2 : nat) P Q : Lemma wp_le E (n1 n2 : Z) P Q :
(n1 n2 P Q (LitV $ LitBool true)) (n1 n2 P Q (LitV $ LitBool true))
(n2 < n1 P Q (LitV $ LitBool false)) (n2 < n1 P Q (LitV $ LitBool false))
P wp E (BinOp LeOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q. P wp E (BinOp LeOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Q.
Proof. Proof.
intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 n2)); by eauto with omega. destruct (bool_decide_reflect (n1 n2)); by eauto with omega.
Qed. Qed.
Lemma wp_lt E (n1 n2 : nat) P Q : Lemma wp_lt E (n1 n2 : Z) P Q :
(n1 < n2 P Q (LitV $ LitBool true)) (n1 < n2 P Q (LitV $ LitBool true))
(n2 n1 P Q (LitV $ LitBool false)) (n2 n1 P Q (LitV $ LitBool false))
P wp E (BinOp LtOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q. P wp E (BinOp LtOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Q.
Proof. Proof.
intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed. Qed.
Lemma wp_eq E (n1 n2 : nat) P Q : Lemma wp_eq E (n1 n2 : Z) P Q :
(n1 = n2 P Q (LitV $ LitBool true)) (n1 = n2 P Q (LitV $ LitBool true))
(n1 n2 P Q (LitV $ LitBool false)) (n1 n2 P Q (LitV $ LitBool false))
P wp E (BinOp EqOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q. P wp E (BinOp EqOp (Lit $ LitInt n1) (Lit $ LitInt n2)) Q.
Proof. Proof.
intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
......
...@@ -2,13 +2,15 @@ Require Export program_logic.language prelude.strings. ...@@ -2,13 +2,15 @@ Require Export program_logic.language prelude.strings.
Require Import prelude.gmap. Require Import prelude.gmap.
Module heap_lang. Module heap_lang.
Open Scope Z_scope.
(** Expressions and vals. *) (** Expressions and vals. *)
Definition loc := positive. (* Really, any countable type. *) Definition loc := positive. (* Really, any countable type. *)
Inductive base_lit : Set := Inductive base_lit : Set :=
| LitNat (n : nat) | LitBool (b : bool) | LitUnit. | LitInt (n : Z) | LitBool (b : bool) | LitUnit.
Inductive un_op : Set := Inductive un_op : Set :=
| NegOp. | NegOp | MinusUnOp.
Inductive bin_op : Set := Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | LtOp | EqOp. | PlusOp | MinusOp | LeOp | LtOp | EqOp.
...@@ -152,16 +154,17 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr := ...@@ -152,16 +154,17 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit := Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
match op, l with match op, l with
| NegOp, LitBool b => Some (LitBool (negb b)) | NegOp, LitBool b => Some (LitBool (negb b))
| MinusUnOp, LitInt n => Some (LitInt (- n))
| _, _ => None | _, _ => None
end. end.
Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit := Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
match op, l1, l2 with match op, l1, l2 with
| PlusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 + n2) | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
| MinusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 - n2) | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
| LeOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 n2) | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 n2)
| LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 < n2) | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2)
| EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 = n2) | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2)
| _, _, _ => None | _, _, _ => None
end. end.
......
...@@ -4,7 +4,7 @@ Delimit Scope lang_scope with L. ...@@ -4,7 +4,7 @@ Delimit Scope lang_scope with L.
Bind Scope lang_scope with expr val. Bind Scope lang_scope with expr val.
Arguments wp {_ _} _ _%L _. Arguments wp {_ _} _ _%L _.
Coercion LitNat : nat >-> base_lit. Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit. Coercion LitBool : bool >-> base_lit.
(** No coercion from base_lit to expr. This makes is slightly easier to tell (** No coercion from base_lit to expr. This makes is slightly easier to tell
apart language and Coq expressions. *) apart language and Coq expressions. *)
...@@ -22,6 +22,8 @@ Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L) ...@@ -22,6 +22,8 @@ Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
(at level 50, left associativity) : lang_scope. (at level 50, left associativity) : lang_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L) Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
(at level 50, left associativity) : lang_scope. (at level 50, left associativity) : lang_scope.
Notation "- e" := (UnOp MinusUnOp e%L) (at level 35, right associativity) : lang_scope.
Notation "~ e" := (UnOp NegOp e%L) (at level 75, right associativity) : lang_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope.
Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope.
Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope. Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
......
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