1 files changed, 76 insertions, 0 deletions
diff --git a/minijazz/src/global/static_utils.ml b/minijazz/src/global/static_utils.ml
new file mode 100644
index 0000000..f95ce30
--- /dev/null
+++ b/minijazz/src/global/static_utils.ml
@@ -0,0 +1,76 @@
+open Static
+
+let pow a n =
+  let rec g p x = function
+  | 0 -> x
+  | i ->
+      g (p * p) (if i mod 2 = 1 then p * x else x) (i/2)
+  in
+  g a 1 n
+;;
+
+
+let fun_of_op op = match op with
+  | SAdd -> (+) | SMinus -> (-)
+  | SMult -> (fun i1 i2 -> i1 * i2)
+  | SDiv -> (/)
+  | SPower -> pow
+  | _ -> assert false
+
+let fun_of_comp_op op = match op with
+  | SEqual -> (=) | SLeq -> (<=)  | SLess -> (<)
+  | _ -> assert false
+
+let rec simplify env se = match se.se_desc with
+  | SInt _ | SBool _ -> se
+  | SVar n ->
+      (try
+         let se = NameEnv.find n env in
+         simplify env se
+        with
+          | Not_found -> se)
+  | SBinOp(op, se1, se2) ->
+      let se1 = simplify env se1 in
+      let se2 = simplify env se2 in
+      let desc =
+        match op, se1.se_desc, se2.se_desc with
+          | (SAdd | SMinus | SDiv  | SMult | SPower), SInt i1, SInt i2 ->
+              let f = fun_of_op op in
+              SInt (f i1 i2)
+        | (SEqual | SLess | SLeq | SGreater | SGeq), SInt i1, SInt i2 ->
+            let f = fun_of_comp_op op in
+            SBool (f i1 i2)
+        | _, _, _ -> SBinOp(op, se1, se2)
+      in
+      { se with se_desc = desc }
+  | SIf(c, se1, se2) ->
+      let c = simplify env c in
+      let se1 = simplify env se1 in
+      let se2 = simplify env se2 in
+      (match c.se_desc, se1.se_desc, se2.se_desc with
+        | SBool true, _, _ -> se1
+        | SBool false, _, _ -> se2
+        | _, sed1, sed2 when sed1 = sed2 -> { se with se_desc = sed1 }
+        | _, _, _ -> { se with se_desc = SIf(c, se1, se2) })
+
+let rec subst env se = match se.se_desc with
+  | SInt _ | SBool _ -> se
+  | SVar n ->
+      (try
+          NameEnv.find n env
+        with
+          | Not_found -> se)
+  | SBinOp(op, se1, se2) ->
+      { se with se_desc = SBinOp(op, subst env se1, subst env se2) }
+  | SIf(c, se1, se2) ->
+      { se with se_desc = SIf(subst env c, subst env se1, subst env se2) }
+
+exception Unsatisfiable of static_exp
+let check_true env cl =
+  let check_one c =
+    let res = simplify env c in
+    match res.se_desc with
+      | SBool true -> ()
+      | _ -> raise (Unsatisfiable c)
+  in
+  List.iter check_one cl