Merge pull request #3809 from mtzguido/reals

Primops.Real: more simplifications

Author: mtzguido

src/basic/FStarC.Real.fst

@@ -14,3 +14,45 @@
    limitations under the License.
 *)
 module FStarC.Real
+
+module Z = FStarC.BigInt
+
+let rec dropWhile f xs =
+  match xs with
+  | [] -> []
+  | x::xs ->
+    if f x
+    then dropWhile f xs
+    else x::xs
+
+let int_frac (r : real): option (string & string) =
+  match String.split ['.'] r._0 with
+  | [i; f] ->
+    let i = String.list_of_string i in
+    let f = String.list_of_string f in
+    let i = i |> dropWhile (fun c -> c = '0') in
+    let f = f |> List.rev |> dropWhile (fun c -> c = '0') |> List.rev in
+    Some (String.string_of_list i, String.string_of_list f)
+  | _ -> None
+
+let max x y =
+  if x > y then x else y
+
+let zeropad_match (f1 : string) (f2 : string): string & string =
+  let len = max (String.length f1) (String.length f2) in
+  let f1 = f1 ^ String.make (len - String.length f1) '0' in
+  let f2 = f2 ^ String.make (len - String.length f2) '0' in
+  f1, f2
+
+let cmp (r1 r2 : real) : option order =
+  match int_frac r1, int_frac r2 with
+  | Some (i1, f1), Some (i2, f2) ->
+    let f1, f2 = zeropad_match f1 f2 in
+    let i1 = Z.to_int_fs <| Z.big_int_of_string i1 in
+    let i2 = Z.to_int_fs <| Z.big_int_of_string i2 in
+    let f1 = Z.to_int_fs <| Z.big_int_of_string f1 in
+    let f2 = Z.to_int_fs <| Z.big_int_of_string f2 in
+    Some <| FStarC.Class.Ord.cmp (i1, f1) (i2, f2) // lex order
+
+  | _ ->
+    None

src/basic/FStarC.Real.fsti

@@ -15,7 +15,13 @@
 *)
 module FStarC.Real
 
+open FStarC.Effect
+open FStarC.Order
+
 (* A type for embedded real constants. This allows to write embeddings for them
 (see FStarC.Syntax.Embeddings and FStarC.TypeChecker.NBETerm). *)
 
 type real = | Real of string
+
+(* Compares two reals, may return None if unknown. *)
+val cmp (r1 r2 : real) : option order

src/typechecker/FStarC.TypeChecker.Primops.Real.fst

@@ -59,27 +59,14 @@ instance nbe_e_tf : TypeChecker.NBETerm.embedding tf =
   in
   mk_emb em un (fun () -> lid_as_typ PC.bool_lid [] []) (Syntax.Embeddings.emb_typ_of tf)
 
-let cmp (r1 r2 : Real.real) : option order =
-  match r1._0, r2._0 with
-  | "0.0", "0.0" -> Some Eq
-  | "0.0", "0.5" -> Some Lt
-  | "0.0", "1.0" -> Some Lt
-  | "0.5", "0.0" -> Some Gt
-  | "0.5", "0.5" -> Some Eq
-  | "0.5", "1.0" -> Some Lt
-  | "1.0", "0.0" -> Some Gt
-  | "1.0", "0.5" -> Some Gt
-  | "1.0", "1.0" -> Some Eq
-  | _ -> None
-
 let lt (r1 r2 : Real.real) : option tf =
-  cmp r1 r2 |> Class.Monad.fmap (function Lt -> T | _ -> F)
+  Real.cmp r1 r2 |> Class.Monad.fmap (function Lt -> T | _ -> F)
 let le (r1 r2 : Real.real) : option tf =
-  cmp r1 r2 |> Class.Monad.fmap (function Lt | Eq -> T | _ -> F)
+  Real.cmp r1 r2 |> Class.Monad.fmap (function Lt | Eq -> T | _ -> F)
 let gt (r1 r2 : Real.real) : option tf =
-  cmp r1 r2 |> Class.Monad.fmap (function Gt -> T | _ -> F)
+  Real.cmp r1 r2 |> Class.Monad.fmap (function Gt -> T | _ -> F)
 let ge (r1 r2 : Real.real) : option tf =
-  cmp r1 r2 |> Class.Monad.fmap (function Gt | Eq -> T | _ -> F)
+  Real.cmp r1 r2 |> Class.Monad.fmap (function Gt | Eq -> T | _ -> F)
 
 let of_int (i:Z.t) : Real.real =
   Real.Real (string_of_int (Z.to_int_fs i) ^ ".0")

src/typechecker/FStarC.TypeChecker.TermEqAndSimplify.fst

@@ -164,12 +164,17 @@ let rec eq_tm (env:env_t) (t1:term) (t2:term) : eq_result =
       Unknown
 
     | Tm_constant (Const_real r1), Tm_constant (Const_real r2) ->
-      // We cannot decide equality of reals. Use a conservative approach here.
-      // If the strings match, they are equal, otherwise we don't know. If this
-      // goes via the eq_iff case below, it will falsely claim that "1.0R" and
-      // "01.R" are different, since eq_const does not canonizalize the string
-      // representations.
-      equal_if (r1 = r2)
+      // We cannot simply compare strings (they are not canonicalized, e.g.
+      // "01.R" and "1.0R"). Call the proper comparison in FStarC.Real, which
+      // returns None for unknown.
+      begin match Real.cmp (Real.Real r1) (Real.Real r2) with
+        | Some Order.Eq -> Equal
+        | Some Order.Lt
+        | Some Order.Gt -> NotEqual
+        | None ->
+          // We don't know.
+          Unknown
+      end
 
     | Tm_constant c, Tm_constant d ->
       // NOTE: this relies on the fact that eq_const *correctly decides*

tests/micro-benchmarks/Test.Real.fst

@@ -80,6 +80,11 @@ let _ = assert (0.0R >=. 0.0R)
 let _ = assert (0.0R <=. 0.0R)
 let _ = assert (1.0R >=. 1.0R)
 let _ = assert (1.0R <=. 1.0R)
+let _ = assert (1.0R <=. 2.0R)
+let _ = assert (1.R <=. 1.R)
+let _ = assert (1.R <=. 2.R)
+let _ = assert (1.0R <. 2.0R)
+let _ = assert (1001.0R <. 1002.00R)
 #pop-options
 
 [@@expect_failure] let _ = assert (1.0R <. 0.0R)