/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
   Licensed under the Apache 2.0 License. */

#ifndef KRML_TYPES_H
#define KRML_TYPES_H

#include <inttypes.h>
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>

/* Types which are either abstract, meaning that have to be implemented in C, or
 * which are models, meaning that they are swapped out at compile-time for
 * hand-written C types (in which case they're marked as noextract). */

typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_;
typedef int64_t FStar_Int64_t, FStar_Int64_t_;
typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_;
typedef int32_t FStar_Int32_t, FStar_Int32_t_;
typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_;
typedef int16_t FStar_Int16_t, FStar_Int16_t_;
typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_;
typedef int8_t FStar_Int8_t, FStar_Int8_t_;

/* Only useful when building Kremlib, because it's in the dependency graph of
 * FStar.Int.Cast. */
typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
typedef int64_t FStar_Int63_t, FStar_Int63_t_;

typedef double FStar_Float_float;
typedef uint32_t FStar_Char_char;
typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;

typedef void *FStar_Dyn_dyn;

typedef const char *C_String_t, *C_String_t_, *C_Compat_String_t, *C_Compat_String_t_;

typedef int exit_code;
typedef FILE *channel;

typedef unsigned long long TestLib_cycles;

typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan;

/* Now Prims.string is no longer illegal with the new model in LowStar.Printf;
 * it's operations that produce Prims_string which are illegal. Bring the
 * definition into scope by default. */
typedef const char *Prims_string;

#if (defined(_MSC_VER) && defined(_M_X64) && !defined(__clang__))
#define IS_MSVC64 1
#endif

/* This code makes a number of assumptions and should be refined. In particular,
 * it assumes that: any non-MSVC amd64 compiler supports int128. Maybe it would
 * be easier to just test for defined(__SIZEOF_INT128__) only? */
#if (defined(__x86_64__) ||                                          \
     defined(__x86_64) ||                                            \
     defined(__aarch64__) ||                                         \
     (defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) ||       \
     defined(__s390x__) ||                                           \
     (defined(_MSC_VER) && defined(_M_X64) && defined(__clang__)) || \
     (defined(__mips__) && defined(__LP64__)) ||                     \
     (defined(__riscv) && __riscv_xlen == 64) ||                     \
     defined(__SIZEOF_INT128__))
#define HAS_INT128 1
#endif

/* The uint128 type is a special case since we offer several implementations of
 * it, depending on the compiler and whether the user wants the verified
 * implementation or not. */
#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64)
#include <emmintrin.h>
typedef __m128i FStar_UInt128_uint128;
#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128)
typedef unsigned __int128 FStar_UInt128_uint128;
#else
typedef struct FStar_UInt128_uint128_s {
    uint64_t low;
    uint64_t high;
} FStar_UInt128_uint128;
#endif

/* The former is defined once, here (otherwise, conflicts for test-c89. The
 * latter is for internal use. */
typedef FStar_UInt128_uint128 FStar_UInt128_t, uint128_t;

#include "kremlin/lowstar_endianness.h"

#endif

/* Avoid a circular loop: if this header is included via FStar_UInt8_16_32_64,
 * then don't bring the uint128 definitions into scope. */
#ifndef __FStar_UInt_8_16_32_64_H

#if !defined(KRML_VERIFIED_UINT128) && defined(IS_MSVC64)
#include "fstar_uint128_msvc.h"
#elif !defined(KRML_VERIFIED_UINT128) && defined(HAS_INT128)
#include "fstar_uint128_gcc64.h"
#else
#include "FStar_UInt128_Verified.h"
#include "fstar_uint128_struct_endianness.h"
#endif

#endif