Some basic simplification rules for reals

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

@@ -0,0 +1,98 @@
+module FStar.TypeChecker.Primops.Real
+
+open FStar
+open FStar.Compiler
+open FStar.Compiler.Effect
+open FStar.Compiler.List
+open FStar.Class.Monad
+open FStar.Compiler.Order
+
+open FStar.TypeChecker.Primops.Base
+open FStar.Syntax.Syntax
+open FStar.Syntax.Embeddings
+
+module PC = FStar.Parser.Const
+module Z = FStar.BigInt
+module S = FStar.Syntax.Syntax
+module U = FStar.Syntax.Util
+
+(* Range ops *)
+
+type tf =
+  | T
+  | F
+
+instance e_tf : Syntax.Embeddings.embedding tf =
+  let ty = U.fvar_const PC.prop_lid in
+  let emb_t_prop = ET_app(PC.prop_lid |> Ident.string_of_lid, []) in
+  let em (p:tf) (rng:Range.range) _shadow _norm : term =
+    match p with
+    | T -> U.t_true
+    | F -> U.t_false
+  in
+  let un (t:term) _norm : option tf =
+    match (unmeta_div_results t).n with
+    | Tm_fvar fv when FStar.Syntax.Syntax.fv_eq_lid fv PC.true_lid -> Some T
+    | Tm_fvar fv when FStar.Syntax.Syntax.fv_eq_lid fv PC.false_lid -> Some F
+    | _ -> None
+  in
+  mk_emb_full
+      em
+      un
+      (fun () -> ty)
+      (function T -> "T" | F -> "F")
+      (fun () -> emb_t_prop)
+
+instance nbe_e_tf : TypeChecker.NBETerm.embedding tf =
+  let open FStar.TypeChecker.NBETerm in
+  let lid_as_typ l us args =
+    mkFV (lid_as_fv l None) us args
+  in
+  let em _cb a =
+    match a with
+    | T -> lid_as_typ PC.true_lid [] []
+    | F -> lid_as_typ PC.false_lid [] []
+  in
+  let un _cb t =
+    match t.nbe_t with
+    | FV (fv, [], []) when fv_eq_lid fv PC.true_lid -> Some T
+    | FV (fv, [], []) when fv_eq_lid fv PC.false_lid -> Some F
+    | _ -> None
+  in
+  mk_emb em un (fun () -> lid_as_typ PC.bool_lid [] []) (Syntax.Embeddings.emb_typ_of tf)
+
+let cmp (r1 r2 : Compiler.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 : Compiler.Real.real) : option tf =
+  cmp r1 r2 |> Class.Monad.fmap (function Lt -> T | _ -> F)
+let le (r1 r2 : Compiler.Real.real) : option tf =
+  cmp r1 r2 |> Class.Monad.fmap (function Lt | Eq -> T | _ -> F)
+let gt (r1 r2 : Compiler.Real.real) : option tf =
+  cmp r1 r2 |> Class.Monad.fmap (function Gt -> T | _ -> F)
+let ge (r1 r2 : Compiler.Real.real) : option tf =
+  cmp r1 r2 |> Class.Monad.fmap (function Gt | Eq -> T | _ -> F)
+
+let of_int (i:Z.t) : Compiler.Real.real =
+  Compiler.Real.Real (string_of_int (Z.to_int_fs i) ^ ".0")
+
+let ops = [
+  mk1 0 PC.real_of_int of_int;
+]
+
+let simplify_ops = [
+  mk2' 0 PC.real_op_LT  lt lt;
+  mk2' 0 PC.real_op_LTE le le;
+  mk2' 0 PC.real_op_GT  gt gt;
+  mk2' 0 PC.real_op_GTE ge ge;
+]

src/typechecker/FStar.TypeChecker.Primops.Real.fsti

@@ -0,0 +1,6 @@
+module FStar.TypeChecker.Primops.Real
+
+open FStar.TypeChecker.Primops.Base
+
+val ops : list primitive_step
+val simplify_ops : list primitive_step

src/typechecker/FStar.TypeChecker.Primops.fst

@@ -125,8 +125,10 @@ let built_in_primitive_steps_list : list primitive_step =
   @ Primops.MachineInts.ops
   @ Primops.Errors.Msg.ops
   @ Primops.Range.ops
+  @ Primops.Real.ops
 
 let env_dependent_ops (env:Env.env_t) = Primops.Eq.dec_eq_ops env
 
 let simplification_ops_list (env:Env.env_t) : list primitive_step =
   Primops.Eq.prop_eq_ops env
+  @ Primops.Real.simplify_ops

tests/micro-benchmarks/Test.Real.fst

@@ -70,3 +70,28 @@ let mul_comm = assert (forall x y. x *. y == y *.x)
 let mul_assoc = assert (forall x y z. ((x *. y) *.z) == (x *. (y *. z)))
 let mul_dist = assert (forall x y z. x *. (y +. z) == (x *. y) +. (x *.z))
 #pop-options
+
+(* Testing some simplification rules *)
+#push-options "--no_smt"
+let _ = assert (0.0R <. 1.0R)
+let _ = assert (1.0R >. 0.0R)
+let _ = assert (1.0R >=. 0.0R)
+let _ = assert (0.0R <=. 1.0R)
+let _ = assert (0.0R >=. 0.0R)
+let _ = assert (0.0R <=. 0.0R)
+let _ = assert (1.0R >=. 1.0R)
+let _ = assert (1.0R <=. 1.0R)
+#pop-options
+
+[@@expect_failure] let _ = assert (1.0R <. 0.0R)
+[@@expect_failure] let _ = assert (0.0R >. 1.0R)
+[@@expect_failure] let _ = assert (0.0R >=. 1.0R)
+[@@expect_failure] let _ = assert (1.0R <=. 0.0R)
+
+#push-options "--no_smt"
+let test_ref1 = Some #(r:real{r >. 0.0R}) 1.0R
+let test_ref2 = Some #(r:real{r >. of_int 0}) 1.0R
+#pop-options
+
+// This one does not work witout SMT as zero is not unfolded!
+let test_ref3 = Some #(r:real{r >. zero}) 1.0R