Merge pull request #734 from hacspec/engine-kill-gmp-dependency

refactor(engine/fstar-ast): get rid of `zarith` and GMP

Author: W95Psp

engine/backends/fstar/fstar-surface-ast/FStar_BaseTypes.ml

@@ -1,10 +1,10 @@
 type char   = FStar_Char.char[@@deriving yojson,show]
-type float  = FStar_Float.float[@@deriving yojson,show]
-type double = FStar_Float.double[@@deriving yojson,show]
-type byte   = FStar_UInt8.byte[@@deriving yojson,show]
-type int8   = FStar_Int8.int8
-type uint8  = FStar_UInt8.uint8
-type int16   = FStar_Int16.int16
-type uint16  = FStar_UInt16.uint16
-type int32  = FStar_Int32.int32
-type int64  = FStar_Int64.int64
+type float  = Base.Float.t
+type double = Base.Float.t
+type byte   = Base.Int.t
+type int8   = Stdint.Int8.t
+type uint8  = Stdint.Uint8.t
+type int16   = Stdint.Int16.t
+type uint16  = Stdint.Uint16.t
+type int32  = Stdint.Int32.t
+type int64  = Stdint.Int64.t

engine/backends/fstar/fstar-surface-ast/FStar_BigInt.ml

@@ -1,21 +1,2 @@
 module UChar = BatUChar
-
-module U32 = FStar_UInt32
-
 type char = int[@@deriving yojson,show]
-type char_code = U32.t
-
-(* FIXME(adl) UChar.lowercase/uppercase removed from recent Batteries. Use Camomile? *)
-let lowercase (x:char) : char =
-  try Char.code (Char.lowercase_ascii (Char.chr x))
-  with _ -> x
-
-let uppercase (x:char) : char =
-  try Char.code (Char.uppercase_ascii (Char.chr x))
-  with _ -> x
-
-let int_of_char (x:char) : Z.t= Z.of_int x
-let char_of_int (i:Z.t) : char = Z.to_int i
-
-let u32_of_char (x:char) : char_code = U32.of_native_int x
-let char_of_u32 (x:char_code) : char = U32.to_native_int x