fact: Fixpoint evalPrim {Tl T} (t: ArithExpr Tl T) {struct t} : evalExprTypePrim_list Tl -> evalExprTypePrim T := match t with | Int _ p => fun l => Uint63.of_Z p | BinFl _ x => fun l => x | Var _ n => fun l => @nthExprTypePrim _ Integer n l (Uint63.of_Z 0) | Op Tl' T' OP t1 t2 => fun l => match T' return ArithExpr Tl' T' -> ArithExpr Tl' T' -> evalExprTypePrim T' with | Integer => fun t1' t2' => PIOpToFunction OP (evalPrim t1' l) (evalPrim t2' l) | BinFloat => fun t1' t2' => PFOpToFunction OP (evalPrim t1' l) (evalPrim t2' l) end t1 t2 | OpExact _ OP t1 t2 => fun l => PFOpToFunction OP (evalPrim t1 l) (evalPrim t2 l) | Fma _ t1 t2 t3 | FmaExact _ t1 t2 t3 => fun l => B2Prim (FPfma mode_NE (Prim2B (evalPrim t1 l)) (Prim2B (evalPrim t2 l)) (Prim2B (evalPrim t3 l))) | Nearbyint _ t => fun l => B2Prim (FPnearbyint mode_NE (Prim2B (evalPrim t l))) | FastNearbyint _ t => fun l => (evalPrim t l + 0x1.8p52 - 0x1.8p52)%float | FastNearbyintToInt _ t => fun l => (normfr_mantissa (fst (frshiftexp (evalPrim t l + 0x1.8p52)%float)) - 6755399441055744)%uint63 | TruncToInt _ t => fun l => Uint63.of_Z (FPtrunc (Prim2B (evalPrim t l))) | FloatInj _ t => fun l => let x := evalPrim t l in let absx := Sint63.abs x in let f := PrimFloat.of_uint63 absx in if (0 <=? x)%sint63 then f else PrimFloat.opp f | Sqrt Tl' T' t => fun l => match T' return ArithExpr Tl' T' -> evalExprTypePrim T' with | Integer => fun t' => Uint63.sqrt (evalPrim t' l) | BinFloat => fun t' => PrimFloat.sqrt (evalPrim t' l) end t | Let _ _ _ t1 t2 => fun l => let x := evalPrim t1 l in evalPrim t2 (x, l) | ArrayAcc _ a t => fun l => get a (evalPrim t l) | Assert _ _ _ t | Postcond _ _ _ t => fun l => evalPrim t l end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)