fact: Fixpoint evalFloat {Tl T} (t: ArithExpr Tl T) {struct t} : evalExprTypeFloat_list Tl -> mode -> evalExprTypeFloat T := match t in ArithExpr Tl'' T'' return evalExprTypeFloat_list Tl'' -> mode -> evalExprTypeFloat T'' with | Int _ p => fun l md => Int32.norm p | BinFl _ x => fun l md => Prim2B x | Var _ n => fun l md => @nthExprTypeFloat _ Integer n l 0%Z | Op Tl' T' OP t1 t2 => fun l md => match T' return ArithExpr Tl' T' -> ArithExpr Tl' T' -> evalExprTypeFloat T' with | Integer => fun t1' t2' => SIOpToFunction OP (evalFloat t1' l md) (evalFloat t2' l md) | BinFloat => fun t1' t2' => FPOpToFunction OP md (evalFloat t1' l md) (evalFloat t2' l md) end t1 t2 | OpExact _ OP t1 t2 => fun l md => FPOpToFunction OP md (evalFloat t1 l md) (evalFloat t2 l md) | Fma _ t1 t2 t3 | FmaExact _ t1 t2 t3 => fun l md => FPfma md (evalFloat t1 l md) (evalFloat t2 l md) (evalFloat t3 l md) | Nearbyint _ t => fun l md => FPnearbyint mode_NE (evalFloat t l md) | FastNearbyint _ t => fun l md => FPsub mode_NE (FPadd mode_NE (evalFloat t l md) (Prim2B 0x1.8p52%float)) (Prim2B 0x1.8p52%float) | FastNearbyintToInt _ t => fun l md => Int32.norm (FPtrunc (FPsub mode_NE (FPadd mode_NE (evalFloat t l md) (Prim2B 0x1.8p52%float)) (Prim2B 0x1.8p52%float))) | TruncToInt _ t => fun l md => Int32.norm (FPtrunc (evalFloat t l md)) | FloatInj _ t => fun l md => binnorm mode_NE (evalFloat t l md) 0 | Sqrt Tl' T' t => fun l md => match T' return ArithExpr Tl' T' -> evalExprTypeFloat T' with | Integer => fun t' => Z.sqrt (evalFloat t' l md) | BinFloat => fun t' => FPsqrt md (evalFloat t' l md) end t | Let _ _ _ t1 t2 => fun l md => let x := evalFloat t1 l md in evalFloat t2 (x, l) md | ArrayAcc _ a t => fun l md => Prim2B (get a (of_Z (evalFloat t l md))) | Assert _ _ _ t | Postcond _ _ _ t => fun l md => evalFloat t l md end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)