fpValTree.lem

(*
  Definition of floating point value trees for CakeML
*)
open import Pervasives
open import Lib

type fp_opt = | Opt | NoOpt
type fp_cmp = FP_Less | FP_LessEqual | FP_Greater | FP_GreaterEqual | FP_Equal
type fp_uop = FP_Abs | FP_Neg | FP_Sqrt
type fp_bop = FP_Add | FP_Sub | FP_Mul | FP_Div
type fp_top = | FP_Fma

declare {isabelle} rename type fp_cmp = fp_cmp_op
declare {isabelle} rename type fp_uop = fp_uop_op
declare {isabelle} rename type fp_bop = fp_bop_op
declare {isabelle} rename type fp_top = fp_top_op

type fp_word_val =
     | Fp_const of word64
     | Fp_uop of fp_uop * fp_word_val
     | Fp_bop of fp_bop * fp_word_val * fp_word_val
     | Fp_top of fp_top * fp_word_val * fp_word_val * fp_word_val
     | Fp_wopt of fp_opt * fp_word_val

type fp_bool_val =
     (* | Fp_pred of fp_pred * fp_word_val *)
     | Fp_cmp of fp_cmp * fp_word_val * fp_word_val
     | Fp_bopt of fp_opt * fp_bool_val

(*
val fp_pred: fp_pred -> fp_word_val -> fp_bool_val
let fp_pred fop f1 = Fp_pred fop f1 *)

val fp_cmp : fp_cmp -> fp_word_val -> fp_word_val -> fp_bool_val
let fp_cmp fop f1 f2 = Fp_cmp fop f1 f2

val fp_uop : fp_uop -> fp_word_val -> fp_word_val
let fp_uop fop f1 = Fp_uop fop f1

val fp_bop : fp_bop -> fp_word_val -> fp_word_val -> fp_word_val
let fp_bop fop f1 f2 = Fp_bop fop f1 f2

val fp_top : fp_top -> fp_word_val -> fp_word_val -> fp_word_val -> fp_word_val
let fp_top fop f1 f2 f3 = Fp_top fop f1 f2 f3