Commit c981e6b5 authored by Dan Frumin's avatar Dan Frumin

Get rid of a useless known_locs argument for `dbase_lit_interp`.

parent 0c261f6f
......@@ -38,7 +38,7 @@ Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
| dLocUnknown l => l
end.
Definition dbase_lit_interp (E : known_locs) (l : dbase_lit) : base_lit :=
Definition dbase_lit_interp (l : dbase_lit) : base_lit :=
match l with
| dLitInt x => LitInt x
| dLitBool b => LitBool b
......@@ -48,7 +48,7 @@ Definition dbase_lit_interp (E : known_locs) (l : dbase_lit) : base_lit :=
Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
match v with
| dLitV l => LitV (dbase_lit_interp E l)
| dLitV l => LitV (dbase_lit_interp l)
| dPairV dv1 dv2 => PairV (dval_interp E dv1) (dval_interp E dv2)
| dLocV dl => cloc_to_val (dloc_interp E dl)
| dValUnknown v => v
......@@ -71,8 +71,8 @@ Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
| EqOp => dLitBool (bool_decide (n1 = n2))
end.
Lemma dbin_op_eval_int_correct E op n1 n2 :
bin_op_eval_int op n1 n2 = dbase_lit_interp E (dbin_op_eval_int op n1 n2).
Lemma dbin_op_eval_int_correct op n1 n2 :
bin_op_eval_int op n1 n2 = dbase_lit_interp (dbin_op_eval_int op n1 n2).
Proof. by destruct op. Qed.
Definition dbin_op_eval_bool
......@@ -87,18 +87,19 @@ Definition dbin_op_eval_bool
| EqOp => Some (dLitBool (bool_decide (b1 = b2)))
end.
Lemma dbin_op_eval_bool_correct E op b1 b2 w :
Lemma dbin_op_eval_bool_correct op b1 b2 w :
dbin_op_eval_bool op b1 b2 = Some w
bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp E w).
bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp w).
Proof. destruct op; simpl; try by inversion 1. Qed.
(* DF: why are we not allowing the `dLocV _, dLocV _` case? *)
Definition dbin_op_eval
(E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
match dv1,dv2 with
| dLitV l1, dLitV l2 =>
if decide (op = EqOp)
then Some $ dLitV $ dLitBool
$ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
$ bool_decide (dbase_lit_interp l1 = dbase_lit_interp l2)
else match l1, l2 with
| dLitInt n1, dLitInt n2 => Some $ dLitV $ dbin_op_eval_int op n1 n2
| dLitBool b1, dLitBool b2 => dLitV <$> dbin_op_eval_bool op b1 b2
......@@ -391,15 +392,15 @@ Global Instance into_cloc_plus_plus l l' i j :
Proof. rewrite /IntoCLocPlus=> ->. by rewrite cloc_plus_plus. Qed.
(** ** IntoDBaseLit *)
Class IntoDBaseLit (E : known_locs) (l : base_lit) (dl : dbase_lit) :=
into_dbase_lit : l = dbase_lit_interp E dl.
Class IntoDBaseLit (l : base_lit) (dl : dbase_lit) :=
into_dbase_lit : l = dbase_lit_interp dl.
Global Instance into_dbase_lit_int E i :
IntoDBaseLit E (LitInt i) (dLitInt i).
Global Instance into_dbase_lit_int i :
IntoDBaseLit (LitInt i) (dLitInt i).
Proof. split; eauto. Qed.
Global Instance into_dbase_lit_default E l :
IntoDBaseLit E l (dLitUnknown l) | 1000.
Global Instance into_dbase_lit_default l :
IntoDBaseLit l (dLitUnknown l) | 1000.
Proof. split; eauto. Qed.
(** ** ExprIntoDVal *)
......@@ -408,7 +409,7 @@ Class ExprIntoDVal (E : known_locs) (e : expr) (dv : dval) :=
expr_into_dval_wf : dval_wf E dv }.
Global Instance expr_into_dval_lit E l dl :
IntoDBaseLit E l dl ExprIntoDVal E (Lit l) (dLitV dl).
IntoDBaseLit l dl ExprIntoDVal E (Lit l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.
Global Instance expr_into_dval_loc E l k i j :
......@@ -430,7 +431,7 @@ Class IntoDVal (E : known_locs) (v : val) (dv : dval) :=
into_dval_wf : dval_wf E dv }.
Global Instance into_dval_lit E l dl :
IntoDBaseLit E l dl IntoDVal E (LitV l) (dLitV dl).
IntoDBaseLit l dl IntoDVal E (LitV l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.
Global Instance into_dval_loc E l k i j :
......
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