open import Pervasives
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_prompt

type bitvector 'a = mword 'a

(* stub functions emulating the C softfloat interface *)

val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_add _ _ _ = ()

val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_sub _ _ _ = ()

val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_mul _ _ _ = ()

val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_div _ _ _ = ()

val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_add _ _ _ = ()

val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_sub _ _ _ = ()

val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_mul _ _ _ = ()

val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_div _ _ _ = ()


val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_muladd _ _ _ _ = ()

val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_muladd _ _ _ _ = ()


val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_sqrt _ _ = ()

val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_sqrt _ _ = ()


val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_i32 _ _ = ()

val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_ui32 _ _ = ()

val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i32_to_f32 _ _ = ()

val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui32_to_f32 _ _ = ()

val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_i64 _ _ = ()

val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_ui64 _ _ = ()

val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i64_to_f32 _ _ = ()

val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui64_to_f32 _ _ = ()


val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_i32 _ _ = ()

val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_ui32 _ _ = ()

val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i32_to_f64 _ _ = ()

val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui32_to_f64 _ _ = ()

val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_i64 _ _ = ()

val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_ui64 _ _ = ()

val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i64_to_f64 _ _ = ()

val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui64_to_f64 _ _ = ()


val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_f64 _ _ = ()

val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_f32 _ _ = ()


val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f32_lt _ _ = ()

val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f32_le _ _ = ()

val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f32_eq _ _ = ()

val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f64_lt _ _ = ()

val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f64_le _ _ = ()

val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f64_eq _ _ = ()