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