From 99acbee7d010312b51cc3b95cf980fc06f511ebb Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Thu, 14 Oct 2021 12:52:28 +0200
Subject: [PATCH] Change Fixed-point semantics
---
hol4/Infra/MachineTypeScript.sml | 53 +++++++++++++-------
hol4/floverParserScript.sml | 11 ++--
hol4/semantics/ExpressionSemanticsScript.sml | 2 +-
3 files changed, 43 insertions(+), 23 deletions(-)
diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml
index 7945c5e7..5b3abec2 100644
--- a/hol4/Infra/MachineTypeScript.sml
+++ b/hol4/Infra/MachineTypeScript.sml
@@ -16,11 +16,11 @@ val _ = List.app monadsyntax.enable_monad ["option"];
Datatype:
- mType = REAL | M16 | M32 | M64 | F num num (* first num is word length, second is fractional bits *)
+ mType = REAL | M16 | M32 | M64 | F num num bool (* first num is word length, second is fractional bits, bool is for sign of fractional bits *)
End
Definition isFixedPoint_def :
- isFixedPoint (F w f) = T /\
+ isFixedPoint (F w f s) = T /\
isFixedPoint _ = F
End
@@ -29,7 +29,7 @@ Definition maxExponent_def:
(maxExponent (M16) = 15) /\
(maxExponent (M32) = 127) /\
(maxExponent (M64) = 1023) /\
- (maxExponent (F w f) = f)
+ (maxExponent (F w f s) = f)
End
Definition minExponentPos_def:
@@ -37,7 +37,7 @@ Definition minExponentPos_def:
(minExponentPos (M16) = 14) /\
(minExponentPos (M32) = 126) /\
(minExponentPos (M64) = 1022) /\
- (minExponentPos (F w f) = f)
+ (minExponentPos (F w f s) = f)
End
(**
@@ -48,7 +48,7 @@ which simplifies to 2^(e_max) for base 2
Definition maxValue_def:
maxValue (m:mType) =
case m of
- | F w f => &((2n ** (w-1)) - 1) * inv &(2n ** (maxExponent m))
+ | F w f s => &((2n ** (w-1)) - 1) * (if s then &(2n ** (maxExponent m)) else inv (&(2n ** (maxExponent m))))
| _ => (&(2n ** (maxExponent m))):real
End
@@ -57,7 +57,7 @@ End
Definition minValue_pos_def:
minValue_pos (m:mType) =
case m of
- | F w f => 0
+ | F w f s => 0
| _ => inv (&(2n ** (minExponentPos m)))
End
@@ -102,7 +102,7 @@ Definition mTypeToR_def:
| M64 => if (denormal v M64)
then inv (2 pow (minExponentPos M64 + 53))
else inv (2 pow 53)
- | F w f => inv (2 pow f)
+ | F w f s => if s then (2 pow f) else inv (2 pow f)
End
Theorem mTypeToR_simp =
@@ -116,7 +116,7 @@ Definition computeError_def:
computeError v m =
case m of
| REAL => 0
- | F w f => mTypeToR m v
+ | F w f s => mTypeToR m v
| _ => if (denormal v m) then mTypeToR m v else abs v * mTypeToR m v
End
@@ -190,9 +190,16 @@ Definition isMorePrecise_def:
isMorePrecise (m1:mType) (m2:mType) =
case m1, m2 of
| REAL, _ => T
- | F w1 f1, F w2 f2 => w2 <= w1
- | F w f, _ => F
- | _, F w f => F
+ | F w1 f1 s1, F w2 f2 s2 =>
+ if s1 then
+ if s2 then
+ (w2 ≤ w1 ∧ f2 ≤ f1)
+ else
+ (w2 ≤ w1)
+ else if s2 then F
+ else (w2 ≤ w1 ∧ f2 ≤ f1)
+ | F w f s, _ => F
+ | _, F w f s=> F
| M16, M16 => T
| M32, M32 => T
| M32, M16 => T
@@ -207,9 +214,16 @@ End
**)
Definition morePrecise_def:
(morePrecise REAL _ = T) /\
- (morePrecise (F w1 f1) (F w2 f2) = (w2 <= w1)) /\
- (morePrecise (F w f) _ = F) /\
- (morePrecise _ (F w f) = F) /\
+ (morePrecise (F w1 f1 s1) (F w2 f2 s2) =
+ (if s1 then
+ if s2 then
+ (w2 ≤ w1 ∧ f2 ≤ f1)
+ else
+ (w2 ≤ w1)
+ else if s2 then F
+ else (w2 ≤ w1 ∧ f2 ≤ f1))) ∧
+ (morePrecise (F w f s) _ = F) /\
+ (morePrecise _ (F w f s) = F) /\
(morePrecise M16 M16 = T) /\
(morePrecise M32 M32 = T) /\
(morePrecise M32 M16 = T) /\
@@ -227,6 +241,7 @@ Proof
rpt strip_tac
\\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
\\ fs[morePrecise_def]
+ \\ every_case_tac \\ gs[]
QED
Theorem isMorePrecise_morePrecise:
@@ -268,7 +283,7 @@ QED
has to happen in 64 bits
**)
Definition join_fl_def:
- join_fl (F w1 f1) (F w2 f2) = NONE /\
+ join_fl (F w1 f1 s1) (F w2 f2 s2) = NONE /\
join_fl m1 m2 = if (morePrecise m1 m2) then SOME m1 else SOME m2
End
@@ -281,9 +296,9 @@ End
it for floating-points **)
Definition isCompat_def:
isCompat (REAL) (REAL) = T /\
- isCompat (F w1 f1) (F w2 f2) = morePrecise (F w1 f1) (F w2 f2) /\
- isCompat (F _ _) _ = F /\
- isCompat _ (F _ _) = F /\
+ isCompat (F w1 f1 s1) (F w2 f2 s2) = morePrecise (F w2 f2 s2) (F w1 f1 s1) /\
+ isCompat (F _ _ _) _ = F /\
+ isCompat _ (F _ _ _) = F /\
isCompat m1 m2 = (m1 = m2)
End
@@ -328,7 +343,7 @@ Definition validValue_def:
End
Theorem no_underflow_fixed_point:
- !v f w. ~ denormal v (F w f)
+ !v f w. ~ denormal v (F w f s)
Proof
fs[denormal_def, minValue_pos_def, REAL_NOT_LT, REAL_ABS_POS]
QED
diff --git a/hol4/floverParserScript.sml b/hol4/floverParserScript.sml
index b5323b45..5b141fcb 100644
--- a/hol4/floverParserScript.sml
+++ b/hol4/floverParserScript.sml
@@ -90,7 +90,7 @@ val lex_def = tDefine "lex" `
| DCONST 32 :: ts' => DTYPE M32 :: ts'
| DCONST 64 :: ts' => DTYPE M64 :: ts'
| DFIXED :: DCONST w :: DCONST f :: ts' =>
- DTYPE (F w f) :: ts'
+ DTYPE (F w f s) :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => NIL)
@@ -122,16 +122,21 @@ val str_of_num_def = Define `
if n < 10 then STRING (CHR (n + 48)) ""
else str_join (str_of_num (n DIV 10)) (STRING (CHR ( (n MOD 10) + 48)) "")`
+val str_of_bool_def = Define ‘
+ str_of_bool (b:bool) = if b then "T" else "F"’
+
val type_to_string = Define `
(type_to_string (M16) = "MTYPE 16") /\
(type_to_string (M32) = "MTYPE 32") /\
(type_to_string (M64) = "MTYPE 64") /\
- (type_to_string (F w f) =
+ (type_to_string (F w f s) =
str_join "MTYPE "
(str_join ("F ")
(str_join (str_of_num w)
(str_join " "
- (str_of_num f)))))`; (* FIXME *)
+ (str_join (str_of_num f)
+ (str_join " "
+ (str_of_bool s)))))))`; (* FIXME *)
(* (type_to_string (M128) = "MTYPE 128") /\ *)
(* (type_to_string (M256) = "MTYPE 256")`; *)
diff --git a/hol4/semantics/ExpressionSemanticsScript.sml b/hol4/semantics/ExpressionSemanticsScript.sml
index d2db65dc..2df3c51b 100644
--- a/hol4/semantics/ExpressionSemanticsScript.sml
+++ b/hol4/semantics/ExpressionSemanticsScript.sml
@@ -16,7 +16,7 @@ Definition perturb_def:
(* The Real-type has no error *)
perturb (rVal:real) (REAL) (delta:real) = rVal /\
(* Fixed-point numbers have an absolute error *)
- perturb rVal (F w f) delta = rVal + delta /\
+ perturb rVal (F w f s) delta = rVal + delta /\
(* Floating-point numbers have a relative error in the normal range, and an
absolute error in the subnormal range *)
perturb rVal m delta = if (denormal rVal m)
--
GitLab