Merge branch 'master' of gitlab.mpi-sws.org:AVA/FloVer

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 _ = monadsyntax.enable_monadsyntax();
 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

hol4/TypeValidatorScript.sml

@@ -138,7 +138,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
@@ -172,7 +172,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)
@@ -261,7 +261,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)
@@ -284,9 +284,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)
@@ -484,7 +484,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[]
@@ -613,8 +613,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 _`