diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops.ml index bef5dced187..2c2653149dc 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops.ml @@ -457,7 +457,9 @@ let (built_in_primitive_steps_list : FStar_TypeChecker_Primops_MachineInts.ops (FStar_Compiler_List.op_At FStar_TypeChecker_Primops_Errors_Msg.ops - FStar_TypeChecker_Primops_Range.ops)))))))) + (FStar_Compiler_List.op_At + FStar_TypeChecker_Primops_Range.ops + FStar_TypeChecker_Primops_Real.ops))))))))) let (env_dependent_ops : FStar_TypeChecker_Env.env_t -> FStar_TypeChecker_Primops_Base.primitive_step Prims.list) @@ -465,4 +467,8 @@ let (env_dependent_ops : let (simplification_ops_list : FStar_TypeChecker_Env.env_t -> FStar_TypeChecker_Primops_Base.primitive_step Prims.list) - = fun env -> FStar_TypeChecker_Primops_Eq.prop_eq_ops env \ No newline at end of file + = + fun env -> + let uu___ = FStar_TypeChecker_Primops_Eq.prop_eq_ops env in + FStar_Compiler_List.op_At uu___ + FStar_TypeChecker_Primops_Real.simplify_ops \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Real.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Real.ml new file mode 100644 index 00000000000..deecfee41dc --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Real.ml @@ -0,0 +1,200 @@ +open Prims +type tf = + | T + | F +let (uu___is_T : tf -> Prims.bool) = + fun projectee -> match projectee with | T -> true | uu___ -> false +let (uu___is_F : tf -> Prims.bool) = + fun projectee -> match projectee with | F -> true | uu___ -> false +let (e_tf : tf FStar_Syntax_Embeddings_Base.embedding) = + let ty = FStar_Syntax_Util.fvar_const FStar_Parser_Const.prop_lid in + let emb_t_prop = + let uu___ = + let uu___1 = FStar_Ident.string_of_lid FStar_Parser_Const.prop_lid in + (uu___1, []) in + FStar_Syntax_Syntax.ET_app uu___ in + let em p rng _shadow _norm = + match p with + | T -> FStar_Syntax_Util.t_true + | F -> FStar_Syntax_Util.t_false in + let un t _norm = + let uu___ = + let uu___1 = FStar_Syntax_Embeddings_Base.unmeta_div_results t in + uu___1.FStar_Syntax_Syntax.n in + match uu___ with + | FStar_Syntax_Syntax.Tm_fvar fv when + FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.true_lid -> + FStar_Pervasives_Native.Some T + | FStar_Syntax_Syntax.Tm_fvar fv when + FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.false_lid -> + FStar_Pervasives_Native.Some F + | uu___1 -> FStar_Pervasives_Native.None in + FStar_Syntax_Embeddings_Base.mk_emb_full em un (fun uu___ -> ty) + (fun uu___ -> match uu___ with | T -> "T" | F -> "F") + (fun uu___ -> emb_t_prop) +let (nbe_e_tf : tf FStar_TypeChecker_NBETerm.embedding) = + let lid_as_typ l us args = + let uu___ = FStar_Syntax_Syntax.lid_as_fv l FStar_Pervasives_Native.None in + FStar_TypeChecker_NBETerm.mkFV uu___ us args in + let em _cb a = + match a with + | T -> lid_as_typ FStar_Parser_Const.true_lid [] [] + | F -> lid_as_typ FStar_Parser_Const.false_lid [] [] in + let un _cb t = + match t.FStar_TypeChecker_NBETerm.nbe_t with + | FStar_TypeChecker_NBETerm.FV (fv, [], []) when + FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.true_lid -> + FStar_Pervasives_Native.Some T + | FStar_TypeChecker_NBETerm.FV (fv, [], []) when + FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.false_lid -> + FStar_Pervasives_Native.Some F + | uu___ -> FStar_Pervasives_Native.None in + FStar_TypeChecker_NBETerm.mk_emb em un + (fun uu___ -> lid_as_typ FStar_Parser_Const.bool_lid [] []) + (FStar_Syntax_Embeddings_Base.emb_typ_of e_tf) +let (cmp : + FStar_Compiler_Real.real -> + FStar_Compiler_Real.real -> + FStar_Compiler_Order.order FStar_Pervasives_Native.option) + = + fun r1 -> + fun r2 -> + match ((FStar_Compiler_Real.__proj__Real__item___0 r1), + (FStar_Compiler_Real.__proj__Real__item___0 r2)) + with + | ("0.0", "0.0") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Eq + | ("0.0", "0.5") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Lt + | ("0.0", "1.0") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Lt + | ("0.5", "0.0") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Gt + | ("0.5", "0.5") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Eq + | ("0.5", "1.0") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Lt + | ("1.0", "0.0") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Gt + | ("1.0", "0.5") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Gt + | ("1.0", "1.0") -> + FStar_Pervasives_Native.Some FStar_Compiler_Order.Eq + | uu___ -> FStar_Pervasives_Native.None +let (lt : + FStar_Compiler_Real.real -> + FStar_Compiler_Real.real -> tf FStar_Pervasives_Native.option) + = + fun uu___1 -> + fun uu___ -> + (fun r1 -> + fun r2 -> + let uu___ = cmp r1 r2 in + Obj.magic + (FStar_Class_Monad.fmap FStar_Class_Monad.monad_option () () + (fun uu___1 -> + (fun uu___1 -> + let uu___1 = Obj.magic uu___1 in + match uu___1 with + | FStar_Compiler_Order.Lt -> Obj.magic T + | uu___2 -> Obj.magic F) uu___1) (Obj.magic uu___))) + uu___1 uu___ +let (le : + FStar_Compiler_Real.real -> + FStar_Compiler_Real.real -> tf FStar_Pervasives_Native.option) + = + fun uu___1 -> + fun uu___ -> + (fun r1 -> + fun r2 -> + let uu___ = cmp r1 r2 in + Obj.magic + (FStar_Class_Monad.fmap FStar_Class_Monad.monad_option () () + (fun uu___1 -> + (fun uu___1 -> + let uu___1 = Obj.magic uu___1 in + match uu___1 with + | FStar_Compiler_Order.Lt -> Obj.magic T + | FStar_Compiler_Order.Eq -> Obj.magic T + | uu___2 -> Obj.magic F) uu___1) (Obj.magic uu___))) + uu___1 uu___ +let (gt : + FStar_Compiler_Real.real -> + FStar_Compiler_Real.real -> tf FStar_Pervasives_Native.option) + = + fun uu___1 -> + fun uu___ -> + (fun r1 -> + fun r2 -> + let uu___ = cmp r1 r2 in + Obj.magic + (FStar_Class_Monad.fmap FStar_Class_Monad.monad_option () () + (fun uu___1 -> + (fun uu___1 -> + let uu___1 = Obj.magic uu___1 in + match uu___1 with + | FStar_Compiler_Order.Gt -> Obj.magic T + | uu___2 -> Obj.magic F) uu___1) (Obj.magic uu___))) + uu___1 uu___ +let (ge : + FStar_Compiler_Real.real -> + FStar_Compiler_Real.real -> tf FStar_Pervasives_Native.option) + = + fun uu___1 -> + fun uu___ -> + (fun r1 -> + fun r2 -> + let uu___ = cmp r1 r2 in + Obj.magic + (FStar_Class_Monad.fmap FStar_Class_Monad.monad_option () () + (fun uu___1 -> + (fun uu___1 -> + let uu___1 = Obj.magic uu___1 in + match uu___1 with + | FStar_Compiler_Order.Gt -> Obj.magic T + | FStar_Compiler_Order.Eq -> Obj.magic T + | uu___2 -> Obj.magic F) uu___1) (Obj.magic uu___))) + uu___1 uu___ +let (of_int : FStar_BigInt.t -> FStar_Compiler_Real.real) = + fun i -> + let uu___ = + let uu___1 = + let uu___2 = FStar_BigInt.to_int_fs i in Prims.string_of_int uu___2 in + Prims.strcat uu___1 ".0" in + FStar_Compiler_Real.Real uu___ +let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = + let uu___ = + FStar_TypeChecker_Primops_Base.mk1 Prims.int_zero + FStar_Parser_Const.real_of_int FStar_Syntax_Embeddings.e_int + FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real of_int in + [uu___] +let (simplify_ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) + = + let uu___ = + FStar_TypeChecker_Primops_Base.mk2' Prims.int_zero + FStar_Parser_Const.real_op_LT FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real e_tf nbe_e_tf lt lt in + let uu___1 = + let uu___2 = + FStar_TypeChecker_Primops_Base.mk2' Prims.int_zero + FStar_Parser_Const.real_op_LTE FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real e_tf nbe_e_tf le le in + let uu___3 = + let uu___4 = + FStar_TypeChecker_Primops_Base.mk2' Prims.int_zero + FStar_Parser_Const.real_op_GT FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real e_tf nbe_e_tf gt gt in + let uu___5 = + let uu___6 = + FStar_TypeChecker_Primops_Base.mk2' Prims.int_zero + FStar_Parser_Const.real_op_GTE FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real FStar_Syntax_Embeddings.e_real + FStar_TypeChecker_NBETerm.e_real e_tf nbe_e_tf ge ge in + [uu___6] in + uu___4 :: uu___5 in + uu___2 :: uu___3 in + uu___ :: uu___1 \ No newline at end of file diff --git a/src/typechecker/FStar.TypeChecker.Primops.Real.fst b/src/typechecker/FStar.TypeChecker.Primops.Real.fst new file mode 100644 index 00000000000..5cc57daeb50 --- /dev/null +++ b/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; +] diff --git a/src/typechecker/FStar.TypeChecker.Primops.Real.fsti b/src/typechecker/FStar.TypeChecker.Primops.Real.fsti new file mode 100644 index 00000000000..57c56858062 --- /dev/null +++ b/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 diff --git a/src/typechecker/FStar.TypeChecker.Primops.fst b/src/typechecker/FStar.TypeChecker.Primops.fst index 3059b7a6a06..f7019af8e1b 100644 --- a/src/typechecker/FStar.TypeChecker.Primops.fst +++ b/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 diff --git a/tests/micro-benchmarks/Test.Real.fst b/tests/micro-benchmarks/Test.Real.fst index 634bfe71147..4834dbd1ffd 100644 --- a/tests/micro-benchmarks/Test.Real.fst +++ b/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