From 668ae1bc10fc1d9ea4d62ae0a2708a52cd83e211 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 21 Jun 2018 03:19:11 +0100
Subject: Constant folding improvements

---
 src/value2.lem | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

(limited to 'src/value2.lem')

diff --git a/src/value2.lem b/src/value2.lem
index 33416503..d9fd1263 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -70,17 +70,13 @@ type vl =
   | V_record of list (string * vl)
   | V_null (* Used for unitialized values and null pointers in C compilation *)
 
-let primops extern args =
-  match (extern, args) with
-  | ("and_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 && b2)
-  | ("and_bool", [V_nondet; V_bool false]) -> V_bool false
-  | ("and_bool", [V_bool false; V_nondet]) -> V_bool false
-  | ("and_bool", _) -> V_nondet
 
-  | ("or_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 || b2)
-  | ("or_bool", [V_nondet; V_bool true]) -> V_bool true
-  | ("or_bool", [V_bool true; V_nondet]) -> V_bool true
-  | ("or_bool", _) -> V_nondet
+let value_int_op_int op = function
+  | [V_int v1; V_int v2] -> V_int (op v1 v2)
+  | _ -> V_null
+end
 
-  | _ -> failwith ("Unimplemented primitive operation " ^ extern)
-  end
+let value_bool_op_int op = function
+  | [V_int v1; V_int v2] -> V_bool (op v1 v2)
+  | _ -> V_null
+end
-- 
cgit v1.2.3