1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
2    Licensed under the Apache 2.0 License. */
3 
4 #ifndef KRML_TYPES_H
5 #define KRML_TYPES_H
6 
7 #include <inttypes.h>
8 #include <stdio.h>
9 #include <stdlib.h>
10 
11 /* Types which are either abstract, meaning that have to be implemented in C, or
12  * which are models, meaning that they are swapped out at compile-time for
13  * hand-written C types (in which case they're marked as noextract). */
14 
15 typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_;
16 typedef int64_t FStar_Int64_t, FStar_Int64_t_;
17 typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_;
18 typedef int32_t FStar_Int32_t, FStar_Int32_t_;
19 typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_;
20 typedef int16_t FStar_Int16_t, FStar_Int16_t_;
21 typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_;
22 typedef int8_t FStar_Int8_t, FStar_Int8_t_;
23 
24 /* Only useful when building Kremlib, because it's in the dependency graph of
25  * FStar.Int.Cast. */
26 typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
27 typedef int64_t FStar_Int63_t, FStar_Int63_t_;
28 
29 typedef double FStar_Float_float;
30 typedef uint32_t FStar_Char_char;
31 typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;
32 
33 typedef void *FStar_Dyn_dyn;
34 
35 typedef const char *C_String_t, *C_String_t_;
36 
37 typedef int exit_code;
38 typedef FILE *channel;
39 
40 typedef unsigned long long TestLib_cycles;
41 
42 typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan;
43 
44 /* The uint128 type is a special case since we offer several implementations of
45  * it, depending on the compiler and whether the user wants the verified
46  * implementation or not. */
47 #if !defined(KRML_VERIFIED_UINT128) && defined(_MSC_VER) && defined(_M_X64)
48 #  include <emmintrin.h>
49 typedef __m128i FStar_UInt128_uint128;
50 #elif !defined(KRML_VERIFIED_UINT128) && !defined(_MSC_VER)
51 typedef unsigned __int128 FStar_UInt128_uint128;
52 #else
53 typedef struct FStar_UInt128_uint128_s {
54   uint64_t low;
55   uint64_t high;
56 } FStar_UInt128_uint128;
57 #endif
58 
59 typedef FStar_UInt128_uint128 FStar_UInt128_t, FStar_UInt128_t_, uint128_t;
60 
61 #endif
62