Quelle gen_compare.sh Sprache: Shell

#!/usr/bin/env bash
# -*- compile-command: "mv -f compare.v{,~} && ./gen_compare.sh" -*-
set -e

exec > compare.v

cat <<EOF
(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *)
Require Import PrimFloat.
Local Open Scope float_scope.

Definition min_denorm := 0x0.0000000000001p-1022%float.  (* Z.ldexp one (-1074)%Z *)

Definition min_norm := 0x0.4p-1022%float.  (* Z.ldexp_one (-1024)%Z *)

EOF

genTest() {
    if [ $# -ne 10 ]; then
        echo >&2 "genTest expects 10 arguments"
    fi
    OPS=("=?" " "<=?" "?=")
    x="$1"
    y="$2"
    OPS1=("$3" "$4" "$5" "$6")  # for x y
    OPS2=("$7" "$8" "$9" "${10}") # for y x
    for i in {0..3}; do
        op="${OPS[$i]}"
        op1="${OPS1[$i]}"
        op2="${OPS2[$i]}"
        echo "Check (eq_refl : $x $op $y = $op1)."
        echo "Check (eq_refl : $y $op $x = $op2)."
        echo
    done
}

genTest nan nan \
        false false false FNotComparable \
        false false false FNotComparable
genTest nan "- nan" \
        false false false FNotComparable \
        false false false FNotComparable

EQ=(true false true FEq \
    true false true FEq)

genTest one one "${EQ[@]}"
genTest zero zero "${EQ[@]}"
genTest zero "- zero" "${EQ[@]}"
genTest "- zero" "- zero" "${EQ[@]}"
genTest infinity infinity "${EQ[@]}"
genTest "- infinity" "- infinity" "${EQ[@]}"

LT=(false true true FLt \
    false false false FGt)

genTest min_denorm min_norm "${LT[@]}"
genTest min_denorm one "${LT[@]}"
genTest min_norm one "${LT[@]}"
genTest one infinity "${LT[@]}"
genTest "- infinity" infinity "${LT[@]}"
genTest "- infinity" one "${LT[@]}"

quality84%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.