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