driver: some mach modules, more consistent use of BigInt

drivers/rust.drv

 printer "rust"
 
 theory BuiltIn
-  syntax type int "i64" (* TODO use some big int type *)
-  syntax literal int "%1" (* TODO big int *)
+  syntax type int "BigInt"
+  syntax literal int "BigInt::from(%1)"
   syntax predicate (=) "%1 == %2"
 end
 
@@ -18,9 +18,9 @@ theory Bool
 end
 
 module int.Int
-  (* TODO big int *)
-  syntax constant zero "0"
-  syntax constant one "1"
+  prelude "use num::bigint::BigInt;"
+  syntax constant zero "BigInt::zero()"
+  syntax constant one "BigInt::one()"
 
   syntax predicate (<)  "%1 < %2"
   syntax predicate (<=) "%1 <= %2"
@@ -43,20 +43,39 @@ module ref.Ref
   syntax val (:=) "%1 = %2"
 end
 
+module ref.Refint
+  syntax val incr "%1 += 1"
+  syntax val decr "%1 -= 1"
+  syntax val (+=) "%1 += %2"
+  syntax val (-=) "%1 -= %2"
+  syntax val ( *= ) "%1 *= %2"
+end
+
+module int.ComputerDivision
+  syntax val div "%1 / %2"
+  syntax val mod "%1 % %2"
+end
+
+module mach.int.Int
+  syntax val ( / ) "%1 / %2"
+  syntax val ( % ) "%1 % %2"
+end
+
 module mach.int.Int32
+  prelude "use num::ToPrimitive;"
   syntax type     int32     "i32"
 
   syntax literal   int32    "%1"
-  syntax converter of_int   "%1"
+(*   syntax converter of_int   "%1" *)
 
-(*
-  (* TODO bigint *)
-  syntax val of_int "Z.to_int %1"
-  syntax val to_int "Z.of_int %1"
+  syntax val of_int "%1.to_i32()" (* TODO test *)
+  syntax val to_int "BigInt::from(%1)"
 
+(*
   syntax constant min_int32 "Z.of_int min_int"
   syntax constant max_int32 "Z.of_int max_int"
 *)
+
 (* "std::i32::MIN" *)
 (* "std::i32::MAX" *)
 (* i32::min_value() *)
@@ -74,3 +93,47 @@ module mach.int.Int32
   syntax val      (>)       "%1 > %2"
 
 end
+
+module mach.int.Int64
+  prelude "use num::ToPrimitive;"
+
+  syntax type int64 "i64"
+
+  syntax literal int64 "%1"
+(*   syntax converter of_int   "%1" *)
+
+  syntax val of_int "%1.to_i64()" (* TODO test *)
+  syntax val to_int "BigInt::from(%1)"
+
+  syntax constant min_int64 "BigInt::from(i64::min_int())"
+  syntax constant max_int64 "BigInt::from(i64::max_int())"
+(*   syntax constant min_int64 "Z.of_int min_int" *)
+(*   syntax constant max_int64 "Z.of_int max_int" *)
+(*   syntax constant zero      "0i64" *)
+(*   syntax constant one       "1i64" *)
+  syntax val      ( + )     "%1 + %2"
+  syntax val      ( - )     "%1 - %2"
+  syntax val      (-_)      "- %1"
+  syntax val      ( * )     "%1 * %2"
+  syntax val      ( / )     "%1 / %2"
+  syntax val      ( % )     "%1 % %2"
+  syntax val      (=)       "%1 == %2"
+  syntax val      (<=)      "%1 <= %2"
+  syntax val      (<)       "%1 < %2"
+  syntax val      (>=)      "%1 >= %2"
+  syntax val      (>)       "%1 > %2"
+
+end
+
+module mach.array.Array32
+
+  syntax type array "&[%1]"
+
+  syntax val make "&[%2; %1]"
+  syntax val ([]) "%1[%2]"
+  syntax val ([]<-) "%1[%2] = %3"
+  syntax val length "%1.len()"
+  (* TODO functions that may raise exceptions *)
+  (* append, sub, copy etc. *)
+
+end