Merge pull request #97 from monadius/nonlinear

Formal_ineqs updates

Formal_ineqs/arith/arith_cache.hl

@@ -1,12 +1,18 @@
-(* =========================================================== *)
-(* Cached natural arithmetic                                   *)
-(* Author: Alexey Solovyev                                     *)
-(* Date: 2012-10-27                                            *)
-(* =========================================================== *)
+(* ========================================================================== *)
+(*      Formal verification of nonlinear inequalities in HOL Light            *)
+(*                                                                            *)
+(*      Copyright (c) 2012 Alexey Solovyev                                    *)
+(*                                                                            *)
+(*      This file is distributed under the terms of the MIT licence           *)
+(* ========================================================================== *)
+
+(* -------------------------------------------------------------------------- *)
+(* Cached natural arithmetic                                                  *)
+(* -------------------------------------------------------------------------- *)
 
 (* Dependencies *)
-needs "arith_options.hl";;
-needs "arith/arith_num.hl";;
+needs "Formal_ineqs/arith_options.hl";;
+needs "Formal_ineqs/arith/arith_num.hl";;
 
 
 module Arith_cache = struct
@@ -109,34 +115,34 @@ let tm1_tm2_hash tm1 tm2 =
 
 
 (* SUC *)
-let raw_suc_conv_hash tm =
+let raw_suc_conv_hash tm = 
   let _ = suc_counter := !suc_counter + 1 in
 (*  let _ = suc_list := tm :: !suc_list in *)
     Arith_num.raw_suc_conv_hash tm;;
 
 (* x = 0 *)
-let raw_eq0_hash_conv tm =
+let raw_eq0_hash_conv tm = 
   let _ = eq0_counter := !eq0_counter + 1 in
 (*  let _ = eq0_list := tm :: !eq0_list in *)
     Arith_num.raw_eq0_hash_conv tm;;
 
 (* PRE *)
-let raw_pre_hash_conv tm =
+let raw_pre_hash_conv tm = 
   let _ = pre_counter := !pre_counter + 1 in
     Arith_num.raw_pre_hash_conv tm;;
 
 (* x > 0 *)
-let raw_gt0_hash_conv tm =
+let raw_gt0_hash_conv tm = 
   let _ = gt0_counter := !gt0_counter + 1 in
     Arith_num.raw_gt0_hash_conv tm;;
 
 (* x < y *)
-let raw_lt_hash_conv tm =
+let raw_lt_hash_conv tm = 
   let _ = lt_counter := !lt_counter + 1 in
     Arith_num.raw_lt_hash_conv tm;;
 
 (* x <= y *)
-let raw_le_hash_conv tm =
+let raw_le_hash_conv tm = 
   let _ = le_counter := !le_counter + 1 in
   let hash = op_tm_hash tm in
     try
@@ -147,7 +153,7 @@ let raw_le_hash_conv tm =
 	result;;
 
 (* x + y *)
-let raw_add_conv_hash tm =
+let raw_add_conv_hash tm = 
   let _ = add_counter := !add_counter + 1 in
   let hash = op_tm_hash tm in
     try
@@ -158,7 +164,7 @@ let raw_add_conv_hash tm =
 	result;;
 
 (* x - y *)
-let raw_sub_hash_conv tm =
+let raw_sub_hash_conv tm = 
   let _ = sub_counter := !sub_counter + 1 in
   let hash = op_tm_hash tm in
     try
@@ -168,7 +174,7 @@ let raw_sub_hash_conv tm =
       let _ = my_add sub_table hash result in
 	result;;
 
-let raw_sub_and_le_hash_conv tm1 tm2 =
+let raw_sub_and_le_hash_conv tm1 tm2 = 
   let _ = sub_le_counter := !sub_le_counter + 1 in
   let hash = tm1_tm2_hash tm1 tm2 in
     try
@@ -179,7 +185,7 @@ let raw_sub_and_le_hash_conv tm1 tm2 =
 	result;;
 
 (* x * y *)
-let raw_mul_conv_hash tm =
+let raw_mul_conv_hash tm = 
   let _ = mul_counter := !mul_counter + 1 in
   let hash = op_tm_hash tm in
     try
@@ -190,7 +196,7 @@ let raw_mul_conv_hash tm =
 	result;;
 
 (* x / y *)
-let raw_div_hash_conv tm =
+let raw_div_hash_conv tm = 
   let _ = div_counter := !div_counter + 1 in
   let hash = op_tm_hash tm in
     try
@@ -201,11 +207,11 @@ let raw_div_hash_conv tm =
 	result;;
 
 (* EVEN, ODD *)
-let raw_even_hash_conv tm =
+let raw_even_hash_conv tm = 
   let _ = even_counter := !even_counter + 1 in
     Arith_num.raw_even_hash_conv tm;;
 
-let raw_odd_hash_conv tm =
+let raw_odd_hash_conv tm = 
   let _ = odd_counter := !odd_counter + 1 in
     Arith_num.raw_odd_hash_conv tm;;