fact: Fixpoint evalCArithExpr2 t l := match t with | CInt n => IZR n | CBinFl n1 n2 => IZR n1 * Rpow2 n2 | CVar n => nth n l R0 | COp OP t1 t2 => let x1 := evalCArithExpr2 t1 l in let x2 := evalCArithExpr2 t2 l in match OP with | CADD => (evalCArithExpr2 t1 l) + (evalCArithExpr2 t2 l) | CSUB => (evalCArithExpr2 t1 l) - (evalCArithExpr2 t2 l) | CMUL => (evalCArithExpr2 t1 l) * (evalCArithExpr2 t2 l) | CFLTDIV => (evalCArithExpr2 t1 l) / (evalCArithExpr2 t2 l) | CINTDIV => @Rrnd.nearbyint mode_ZR ((evalCArithExpr2 t1 l) / (evalCArithExpr2 t2 l)) end | CRnd md t' => round radix2 (FLT_exp emin prec) (round_mode md) (evalCArithExpr2 t' l) | CNearbyint t' => @Rrnd.nearbyint mode_NE (evalCArithExpr2 t' l) | CTrunc t' => @Rrnd.nearbyint mode_ZR (evalCArithExpr2 t' l) | CLdexp t' p => ((evalCArithExpr2 t' l) * Rpower 2 (evalCArithExpr2 p l)) | CSqrt t' => sqrt (evalCArithExpr2 t' l) end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr