fact: Fixpoint evalRounded {Tl T} (t: ArithExpr Tl T) {struct t} : evalExprTypeRounded_list Tl -> mode -> evalExprTypeRounded T := match t in ArithExpr Tl'' T'' return evalExprTypeRounded_list Tl'' -> mode -> evalExprTypeRounded T'' with | Int _ p => fun l md => p | BinFl _ x => fun l md => SF2R radix2 (Prim2SF x) | Var _ n => fun l md => @nthExprTypeRounded _ Integer n l 0%Z | Op Tl' T' OP t1 t2 => fun l md => match T' return ArithExpr Tl' T' -> ArithExpr Tl' T' -> evalExprTypeRounded T' with | Integer => fun t1' t2' => ZOpToFunction OP (evalRounded t1' l md) (evalRounded t2' l md) | BinFloat => fun t1' t2' => RrndOpToFunction OP md (evalRounded t1' l md) (evalRounded t2' l md) end t1 t2 | OpExact _ OP t1 t2 => fun l md => ROpToFunction OP (evalRounded t1 l md) (evalRounded t2 l md) | Fma _ t1 t2 t3 => fun l md => @Rrnd.fma md (evalRounded t1 l md) (evalRounded t2 l md) (evalRounded t3 l md) | FmaExact _ t1 t2 t3 => fun l md => (evalRounded t1 l md) * (evalRounded t2 l md) + (evalRounded t3 l md) | Nearbyint _ t | FastNearbyint _ t => fun l md => @Rrnd.nearbyint mode_NE (evalRounded t l md) | FastNearbyintToInt _ t => fun l md => ZnearestE (evalRounded t l md) | TruncToInt _ t => fun l md => Ztrunc (evalRounded t l md) | FloatInj _ t => fun l md => IZR (evalRounded t l md) | Sqrt Tl' T' t => fun l md => match T' return ArithExpr Tl' T' -> evalExprTypeRounded T' with | Integer => fun t' => Z.sqrt (evalRounded t' l md) | BinFloat => fun t' => @Rrnd.sqrt md (evalRounded t' l md) end t | Let _ _ _ t1 t2 => fun l md => let x := evalRounded t1 l md in evalRounded t2 (x, l) md | ArrayAcc _ a t => fun l md => SF2R radix2 (Prim2SF (get a (of_Z (evalRounded t l md)))) | Assert _ _ _ t | Postcond _ _ _ t => fun l md => evalRounded t l md end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)