From e97967940b8fe65a5b4e0fca8ee5b463f698d16e Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 3 Jan 2018 18:53:06 +0100 Subject: [PATCH] hoist LitV/Bool in `binop_eval` --- theories/F_mu_ref_conc/lang.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/F_mu_ref_conc/lang.v b/theories/F_mu_ref_conc/lang.v index 3fc614f..e78750b 100644 --- a/theories/F_mu_ref_conc/lang.v +++ b/theories/F_mu_ref_conc/lang.v @@ -108,11 +108,11 @@ Module lang. | Mul, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a * b)) | Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b)) | Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b)) - | Eq, LitV (Nat a), LitV (Nat b) => Some $ if decide (a = b) then LitV (Bool true) else LitV (Bool false) + | Eq, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if decide (a = b) then true else false)) | Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b)) - | Eq, LitV (Loc l1), LitV (Loc l2) => Some $ if decide (l1 = l2) then LitV (Bool true) else LitV (Bool false) - | Le, LitV (Nat a), LitV (Nat b) => Some $ if le_dec a b then LitV (Bool true) else LitV (Bool false) - | Lt, LitV (Nat a), LitV (Nat b) => Some $ if lt_dec a b then LitV (Bool true) else LitV (Bool false) + | Eq, LitV (Loc l1), LitV (Loc l2) => Some $ LitV (Bool (if decide (l1 = l2) then true else false)) + | Le, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if le_dec a b then true else false)) + | Lt, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if lt_dec a b then true else false)) | Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b)) | _,_,_ => None end. -- 2.26.2