Skip to content

GitLab

Commit e9796794 authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

hoist LitV/Bool in `binop_eval`

parent d136c946
Hide whitespace changes
Inline Side-by-side
Showing with 4 additions and 4 deletions
theories/F_mu_ref_conc/lang.v
View file @ e9796794
...@@ -108,11 +108,11 @@ Module lang. ...@@ -108,11 +108,11 @@ Module lang.
| Mul, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a * b)) | Mul, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a * b))
| Add, 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)) | 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 (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) | 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 $ if le_dec a b then LitV (Bool true) else LitV (Bool 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 $ if lt_dec a b then LitV (Bool true) else LitV (Bool 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)) | Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b))
| _,_,_ => None | _,_,_ => None
end. end.
......
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