688 | | {-# RULES |
689 | | "x# +# 0#" forall x#. x# +# 0# = x# |
690 | | "0# +# x#" forall x#. 0# +# x# = x# |
691 | | "x# -# 0#" forall x#. x# -# 0# = x# |
692 | | "x# -# x#" forall x#. x# -# x# = 0# |
693 | | "x# *# 0#" forall x#. x# *# 0# = 0# |
694 | | "0# *# x#" forall x#. 0# *# x# = 0# |
695 | | "x# *# 1#" forall x#. x# *# 1# = x# |
696 | | "1# *# x#" forall x#. 1# *# x# = x# |
697 | | #-} |
698 | | |
699 | | {-# RULES |
700 | | "x# ># x#" forall x#. x# ># x# = False |
701 | | "x# >=# x#" forall x#. x# >=# x# = True |
702 | | "x# ==# x#" forall x#. x# ==# x# = True |
703 | | "x# /=# x#" forall x#. x# /=# x# = False |
704 | | "x# <# x#" forall x#. x# <# x# = False |
705 | | "x# <=# x#" forall x#. x# <=# x# = True |
706 | | #-} |
707 | | |
708 | | {-# RULES |
709 | | "plusFloat x 0.0" forall x#. plusFloat# x# 0.0# = x# |
710 | | "plusFloat 0.0 x" forall x#. plusFloat# 0.0# x# = x# |
711 | | "minusFloat x 0.0" forall x#. minusFloat# x# 0.0# = x# |
712 | | "timesFloat x 1.0" forall x#. timesFloat# x# 1.0# = x# |
713 | | "timesFloat 1.0 x" forall x#. timesFloat# 1.0# x# = x# |
714 | | "divideFloat x 1.0" forall x#. divideFloat# x# 1.0# = x# |
715 | | #-} |
716 | | |
717 | | {-# RULES |
718 | | "plusDouble x 0.0" forall x#. (+##) x# 0.0## = x# |
719 | | "plusDouble 0.0 x" forall x#. (+##) 0.0## x# = x# |
720 | | "minusDouble x 0.0" forall x#. (-##) x# 0.0## = x# |
721 | | "timesDouble x 1.0" forall x#. (*##) x# 1.0## = x# |
722 | | "timesDouble 1.0 x" forall x#. (*##) 1.0## x# = x# |
723 | | "divideDouble x 1.0" forall x#. (/##) x# 1.0## = x# |
724 | | #-} |
725 | | |
726 | | {- |
727 | | We'd like to have more rules, but for example: |
728 | | |
729 | | This gives wrong answer (0) for NaN - NaN (should be NaN): |
730 | | "minusDouble x x" forall x#. (-##) x# x# = 0.0## |
731 | | |
732 | | This gives wrong answer (0) for 0 * NaN (should be NaN): |
733 | | "timesDouble 0.0 x" forall x#. (*##) 0.0## x# = 0.0## |
734 | | |
735 | | This gives wrong answer (0) for NaN * 0 (should be NaN): |
736 | | "timesDouble x 0.0" forall x#. (*##) x# 0.0## = 0.0## |
737 | | |
738 | | These are tested by num014. |
739 | | |
740 | | Similarly for Float (#5178): |
741 | | |
742 | | "minusFloat x x" forall x#. minusFloat# x# x# = 0.0# |
743 | | "timesFloat0.0 x" forall x#. timesFloat# 0.0# x# = 0.0# |
744 | | "timesFloat x 0.0" forall x#. timesFloat# x# 0.0# = 0.0# |
745 | | -} |
746 | | |