diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml
index 5b3abec2fd3d6798edab0ac0dc280549fe5d0ed1..1802af5fe9a7d240a7bb60eeae0533307acb4e6b 100644
--- a/hol4/Infra/MachineTypeScript.sml
+++ b/hol4/Infra/MachineTypeScript.sml
@@ -4,7 +4,7 @@
@author: Raphael Monat
@maintainer: Heiko Becker
**)
-open realTheory realLib;
+open realTheory realLib integerTheory;
open RealSimpsTheory;
open preambleFloVer;
@@ -16,7 +16,15 @@ val _ = List.app monadsyntax.enable_monad ["option"];
Datatype:
- 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 *)
+ mType = REAL
+ (* Floating point formats *)
+ | M16 | M32 | M64
+ (* Fixed point formats:
+ * first num is word length,
+ * second is fractional bits,
+ * bool is for sign of fractional bits, inverse of the exponent sign with T <=> positive
+ *)
+ | F num num bool
End
Definition isFixedPoint_def :
@@ -181,9 +189,8 @@ QED
REAL is real-valued evaluation, hence the most precise.
All floating-point types are compared by
mTypeToQ m1 <= mTypeToQ m2
- All fixed-point types are compared by comparing only the word size
- We consider a 32 bit fixed-point number to be more precise than a 16 bit
- fixed-point number, no matter what the fractional bits may be.
+ All fixed-point types are compared by comparing the positions of the
+ least and most significant bits. It is equivalent to a subset check.
For the moment, fixed-point and floating-point formats are incomparable.
**)
Definition isMorePrecise_def:
@@ -191,13 +198,8 @@ Definition isMorePrecise_def:
case m1, m2 of
| REAL, _ => T
| 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)
+ let exp1: int = if s1 then &f1 else -&f1 ; exp2 = if s2 then &f2 else -&f2 in
+ &w2 + exp2 <= &w1 + exp1 /\ exp1 <= exp2
| F w f s, _ => F
| _, F w f s=> F
| M16, M16 => T
@@ -215,13 +217,8 @@ End
Definition morePrecise_def:
(morePrecise REAL _ = T) /\
(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))) ∧
+ let exp1: int = if s1 then &f1 else -&f1 ; exp2 = if s2 then &f2 else -&f2 in
+ &w2 + exp2 <= &w1 + exp1 /\ exp1 <= exp2) /\
(morePrecise (F w f s) _ = F) /\
(morePrecise _ (F w f s) = F) /\
(morePrecise M16 M16 = T) /\
@@ -241,7 +238,7 @@ Proof
rpt strip_tac
\\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
\\ fs[morePrecise_def]
- \\ every_case_tac \\ gs[]
+ \\ ntac 2 $ dxrule_all INT_LE_TRANS \\ simp[]
QED
Theorem isMorePrecise_morePrecise:
@@ -305,7 +302,7 @@ End
Definition isJoin_def:
isJoin m1 m2 mj =
if (isFixedPoint m1 /\ isFixedPoint m2)
- then morePrecise m1 mj /\ morePrecise m2 mj
+ then morePrecise mj m1 /\ morePrecise mj m2
else
(case join_fl m1 m2 of
|NONE => F
@@ -315,7 +312,7 @@ End
Definition isJoin3_def:
isJoin3 m1 m2 m3 mj =
if (isFixedPoint m1 /\ isFixedPoint m2 /\ isFixedPoint m3)
- then morePrecise m1 mj /\ morePrecise m2 mj /\ morePrecise m3 mj
+ then morePrecise mj m1 /\ morePrecise mj m2 /\ morePrecise mj m3
else
(case join_fl3 m1 m2 m3 of
|NONE => F
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index 4e6676a30108e16321bd4a434f8045f9f076faa5..38cc3482cd370d92d70591d0983b10ce035bc9a8 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -131,7 +131,7 @@ Definition getValidMap_def:
case mOldO of
| NONE => Fail "Undefined fixed-point type"
| SOME mj =>
- if (morePrecise t1 mj /\ morePrecise t2 mj)
+ if (morePrecise mj t1 /\ morePrecise mj t2)
then addMono e mj akk2_map
else Fail "Incorrect fixed-point type"
else
@@ -165,7 +165,7 @@ Definition getValidMap_def:
case mOldO of
| NONE => Fail "Undefined fixed-point type"
| SOME mj =>
- if (morePrecise t1 mj /\ morePrecise t2 mj /\ morePrecise t3 mj)
+ if (morePrecise mj t1 /\ morePrecise mj t2 /\ morePrecise mj t3)
then addMono e mj akk3_map
else Fail "Incorrect fixed-point type"
else if (t1 = REAL ∨ t2 = REAL ∨ t3 = REAL)
@@ -254,7 +254,7 @@ Proof
\\ Cases_on `getValidMap Gamma e1 akk` \\ fs[result_bind_def]
\\ Cases_on `getValidMap Gamma e2 a` \\ fs[option_case_eq]
\\ Cases_on `isFixedPoint t1` \\ Cases_on `isFixedPoint t2` \\ fs[option_case_eq]
- >- (Cases_on `morePrecise t1 mj` \\ Cases_on `morePrecise t2 mj`
+ >- (Cases_on `morePrecise mj t1` \\ Cases_on `morePrecise mj t2`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ res_tac
\\ by_monotonicity)
@@ -277,9 +277,9 @@ Proof
\\ Cases_on `isFixedPoint t2`
\\ Cases_on `isFixedPoint t3`
\\ fs[option_case_eq]
- >- (Cases_on `morePrecise t1 mj`
- \\ Cases_on `morePrecise t2 mj`
- \\ Cases_on `morePrecise t3 mj`
+ >- (Cases_on `morePrecise mj t1`
+ \\ Cases_on `morePrecise mj t2`
+ \\ Cases_on `morePrecise mj t3`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ res_tac
\\ by_monotonicity)
@@ -475,7 +475,7 @@ Proof
by (rpt strip_tac \\ first_x_assum irule \\ fs[]
\\ qexistsl_tac [`Gamma`, `a`] \\ fs[])
\\ Cases_on ‘isFixedPoint x ∧ isFixedPoint x'’
- >- (fs[option_case_eq] \\ Cases_on `morePrecise x mj` \\ Cases_on `morePrecise x' mj`
+ >- (fs[option_case_eq] \\ Cases_on `morePrecise mj x` \\ Cases_on `morePrecise mj x'`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
\\ reverse (Cases_on `e'' = Binop b e1 e2`) \\ fs[]
@@ -604,8 +604,8 @@ Proof
\\ qexistsl_tac [`Gamma`, `map2`] \\ fs[])
\\ Cases_on `isFixedPoint x /\ isFixedPoint x' /\ isFixedPoint x''`
>- (fs[option_case_eq]
- \\ Cases_on `morePrecise x mj` \\ Cases_on `morePrecise x' mj`
- \\ Cases_on `morePrecise x'' mj`
+ \\ Cases_on `morePrecise mj x` \\ Cases_on `morePrecise mj x'`
+ \\ Cases_on `morePrecise mj x''`
\\ fs[addMono_def, option_case_eq]
\\ rveq \\ fs[FloverMapTree_mem_def, map_find_add]
\\ rename1 `if eNew = Fma e1 e2 e3 then SOME mj else _`