diff --git a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml
index a912bf87e70..8ad61e09d44 100644
--- a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml
+++ b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml
@@ -116,7 +116,9 @@ let build_constant (c: mlconstant): Parsetree.constant =
| FStar_Const.Int16 -> with_w "16"
| FStar_Const.Int32 -> with_w "32"
| FStar_Const.Int64 -> with_w "64"
- | FStar_Const.Sizet -> with_w "64" in
+ | FStar_Const.Int128 -> failwith "128bit machine integer constants should not reach ML ast"
+ | FStar_Const.Sizet -> with_w "64"
+ in
match c with
| MLC_Int (v, None) ->
let s = match Z.of_string v with
diff --git a/ocaml/fstar-lib/generated/FStar_Compiler_MachineInts.ml b/ocaml/fstar-lib/generated/FStar_Compiler_MachineInts.ml
index 5ce3ce72f38..c54348db9f5 100644
--- a/ocaml/fstar-lib/generated/FStar_Compiler_MachineInts.ml
+++ b/ocaml/fstar-lib/generated/FStar_Compiler_MachineInts.ml
@@ -47,7 +47,7 @@ let (is_unsigned : machint_kind -> Prims.bool) =
| SizeT -> true
let (is_signed : machint_kind -> Prims.bool) =
fun k -> let uu___ = is_unsigned k in Prims.op_Negation uu___
-let (width : machint_kind -> Prims.int) =
+let (widthn : machint_kind -> Prims.int) =
fun k ->
match k with
| Int8 -> (Prims.of_int (8))
@@ -75,7 +75,7 @@ let (module_name_for : machint_kind -> Prims.string) =
| SizeT -> "SizeT"
let (mask : machint_kind -> FStar_BigInt.t) =
fun k ->
- let uu___ = width k in
+ let uu___ = widthn k in
match uu___ with
| uu___1 when uu___1 = (Prims.of_int (8)) -> FStar_BigInt.of_hex "ff"
| uu___1 when uu___1 = (Prims.of_int (16)) -> FStar_BigInt.of_hex "ffff"
@@ -85,70 +85,38 @@ let (mask : machint_kind -> FStar_BigInt.t) =
FStar_BigInt.of_hex "ffffffffffffffff"
| uu___1 when uu___1 = (Prims.of_int (128)) ->
FStar_BigInt.of_hex "ffffffffffffffffffffffffffffffff"
-let (int_to_t_lid_for : machint_kind -> FStar_Ident.lid) =
+let (signedness : machint_kind -> FStar_Const.signedness) =
fun k ->
- let path =
- let uu___ =
- let uu___1 = module_name_for k in
- let uu___2 =
- let uu___3 =
- let uu___4 = is_unsigned k in
- if uu___4 then "uint_to_t" else "int_to_t" in
- [uu___3] in
- uu___1 :: uu___2 in
- "FStar" :: uu___ in
- FStar_Ident.lid_of_path path FStar_Compiler_Range_Type.dummyRange
-let (int_to_t_for : machint_kind -> FStar_Syntax_Syntax.term) =
- fun k ->
- let lid = int_to_t_lid_for k in
- FStar_Syntax_Syntax.fvar lid FStar_Pervasives_Native.None
-let (__int_to_t_lid_for : machint_kind -> FStar_Ident.lid) =
- fun k ->
- let path =
- let uu___ =
- let uu___1 = module_name_for k in
- let uu___2 =
- let uu___3 =
- let uu___4 = is_unsigned k in
- if uu___4 then "__uint_to_t" else "__int_to_t" in
- [uu___3] in
- uu___1 :: uu___2 in
- "FStar" :: uu___ in
- FStar_Ident.lid_of_path path FStar_Compiler_Range_Type.dummyRange
-let (__int_to_t_for : machint_kind -> FStar_Syntax_Syntax.term) =
+ let uu___ = is_unsigned k in
+ if uu___ then FStar_Const.Unsigned else FStar_Const.Signed
+let (width : machint_kind -> FStar_Const.width) =
fun k ->
- let lid = __int_to_t_lid_for k in
- FStar_Syntax_Syntax.fvar lid FStar_Pervasives_Native.None
+ match k with
+ | Int8 -> FStar_Const.Int8
+ | UInt8 -> FStar_Const.Int8
+ | Int16 -> FStar_Const.Int16
+ | UInt16 -> FStar_Const.Int16
+ | Int32 -> FStar_Const.Int32
+ | UInt32 -> FStar_Const.Int32
+ | Int64 -> FStar_Const.Int64
+ | UInt64 -> FStar_Const.Int64
+ | UInt128 -> FStar_Const.Int128
+ | SizeT -> FStar_Const.Sizet
type 'k machint =
- | Mk of FStar_BigInt.t * FStar_Syntax_Syntax.meta_source_info
- FStar_Pervasives_Native.option
+ | Mk of FStar_BigInt.t
let (uu___is_Mk : machint_kind -> unit machint -> Prims.bool) =
fun k -> fun projectee -> true
let (__proj__Mk__item___0 : machint_kind -> unit machint -> FStar_BigInt.t) =
- fun k -> fun projectee -> match projectee with | Mk (_0, _1) -> _0
-let (__proj__Mk__item___1 :
- machint_kind ->
- unit machint ->
- FStar_Syntax_Syntax.meta_source_info FStar_Pervasives_Native.option)
- = fun k -> fun projectee -> match projectee with | Mk (_0, _1) -> _1
-let (mk :
- machint_kind ->
- FStar_BigInt.t ->
- FStar_Syntax_Syntax.meta_source_info FStar_Pervasives_Native.option ->
- unit machint)
- = fun k -> fun x -> fun m -> Mk (x, m)
+ fun k -> fun projectee -> match projectee with | Mk _0 -> _0
+let (mk : machint_kind -> FStar_BigInt.t -> unit machint) =
+ fun k -> fun x -> Mk x
let (v : machint_kind -> unit machint -> FStar_BigInt.t) =
- fun k -> fun x -> let uu___ = x in match uu___ with | Mk (v1, uu___1) -> v1
-let (meta :
- machint_kind ->
- unit machint ->
- FStar_Syntax_Syntax.meta_source_info FStar_Pervasives_Native.option)
- =
- fun k ->
- fun x -> let uu___ = x in match uu___ with | Mk (uu___1, meta1) -> meta1
+ fun k -> fun x -> let uu___ = x in match uu___ with | Mk v1 -> v1
+let (int_to_t : machint_kind -> FStar_BigInt.t -> unit machint) =
+ fun k -> fun i -> Mk i
let (make_as :
machint_kind -> unit machint -> FStar_BigInt.t -> unit machint) =
- fun k -> fun x -> fun z -> let uu___ = meta k x in Mk (z, uu___)
+ fun k -> fun x -> fun z -> Mk z
let (showable_bounded_k :
machint_kind -> unit machint FStar_Class_Show.showable) =
fun k ->
@@ -156,7 +124,7 @@ let (showable_bounded_k :
FStar_Class_Show.show =
(fun uu___ ->
match uu___ with
- | Mk (x, m) ->
+ | Mk x ->
let uu___1 =
let uu___2 =
let uu___3 = FStar_BigInt.to_int_fs x in
@@ -185,65 +153,32 @@ let (e_machint :
let em x rng shadow cb =
let uu___ = x in
match uu___ with
- | Mk (i, m) ->
- let it =
- let uu___1 =
- FStar_Syntax_Embeddings_Base.embed
- FStar_Syntax_Embeddings.e_int i in
- uu___1 rng FStar_Pervasives_Native.None cb in
- let int_to_t = int_to_t_for k in
- let t =
+ | Mk i ->
+ let const =
let uu___1 =
- let uu___2 = FStar_Syntax_Syntax.as_arg it in [uu___2] in
- FStar_Syntax_Syntax.mk_Tm_app int_to_t uu___1 rng in
- with_meta_ds rng t m in
- let un uu___1 uu___ =
- (fun t ->
- fun cb ->
- let uu___ =
- let uu___1 =
- let uu___2 = FStar_Syntax_Subst.compress t in
- uu___2.FStar_Syntax_Syntax.n in
- match uu___1 with
- | FStar_Syntax_Syntax.Tm_meta
- { FStar_Syntax_Syntax.tm2 = t1;
- FStar_Syntax_Syntax.meta =
- FStar_Syntax_Syntax.Meta_desugared m;_}
- -> (t1, (FStar_Pervasives_Native.Some m))
- | uu___2 -> (t, FStar_Pervasives_Native.None) in
- match uu___ with
- | (t1, m) ->
- let t2 = FStar_Syntax_Util.unmeta_safe t1 in
- let uu___1 =
- let uu___2 = FStar_Syntax_Subst.compress t2 in
- uu___2.FStar_Syntax_Syntax.n in
- (match uu___1 with
- | FStar_Syntax_Syntax.Tm_app
- { FStar_Syntax_Syntax.hd = hd;
- FStar_Syntax_Syntax.args = (a, uu___2)::[];_}
- when
- (let uu___3 = int_to_t_lid_for k in
- FStar_Syntax_Util.is_fvar uu___3 hd) ||
- (let uu___3 = __int_to_t_lid_for k in
- FStar_Syntax_Util.is_fvar uu___3 hd)
- ->
- Obj.magic
- (Obj.repr
- (let a1 = FStar_Syntax_Util.unlazy_emb a in
- let uu___3 =
- FStar_Syntax_Embeddings_Base.try_unembed
- FStar_Syntax_Embeddings.e_int a1 cb in
- FStar_Class_Monad.op_let_Bang
- FStar_Class_Monad.monad_option () ()
- (Obj.magic uu___3)
- (fun uu___4 ->
- (fun a2 ->
- let a2 = Obj.magic a2 in
- Obj.magic
- (FStar_Pervasives_Native.Some
- (Mk (a2, m)))) uu___4)))
- | uu___2 -> Obj.magic (Obj.repr FStar_Pervasives_Native.None)))
- uu___1 uu___ in
+ let uu___2 = FStar_BigInt.string_of_big_int i in
+ let uu___3 =
+ let uu___4 =
+ let uu___5 = signedness k in
+ let uu___6 = width k in (uu___5, uu___6) in
+ FStar_Pervasives_Native.Some uu___4 in
+ (uu___2, uu___3) in
+ FStar_Const.Const_int uu___1 in
+ FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_constant const) rng in
+ let un t cb =
+ let t1 = FStar_Syntax_Util.unmeta_safe t in
+ let uu___ =
+ let uu___1 = FStar_Syntax_Subst.compress t1 in
+ uu___1.FStar_Syntax_Syntax.n in
+ match uu___ with
+ | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_int
+ (str, FStar_Pervasives_Native.Some (s, w))) when
+ (let uu___1 = signedness k in s = uu___1) &&
+ (let uu___1 = width k in w = uu___1)
+ ->
+ let n = FStar_BigInt.big_int_of_string str in
+ FStar_Pervasives_Native.Some (Mk n)
+ | uu___1 -> FStar_Pervasives_Native.None in
FStar_Syntax_Embeddings_Base.mk_emb_full em un
(fun uu___ ->
let uu___1 =
@@ -273,63 +208,31 @@ let (nbe_machint :
let em cbs x =
let uu___ = x in
match uu___ with
- | Mk (i, m) ->
- let it =
- FStar_TypeChecker_NBETerm.embed FStar_TypeChecker_NBETerm.e_int
- cbs i in
- let int_to_t args =
+ | Mk i ->
+ let const =
let uu___1 =
- let uu___2 =
- let uu___3 =
- let uu___4 = __int_to_t_lid_for k in
- FStar_Syntax_Syntax.lid_as_fv uu___4
- FStar_Pervasives_Native.None in
- (uu___3, [], args) in
- FStar_TypeChecker_NBETerm.FV uu___2 in
- FStar_TypeChecker_NBETerm.mk_t uu___1 in
- let t =
- let uu___1 =
- let uu___2 = FStar_TypeChecker_NBETerm.as_arg it in [uu___2] in
- int_to_t uu___1 in
- with_meta_ds t m in
- let un uu___1 uu___ =
- (fun cbs ->
- fun a ->
- let uu___ =
- match a.FStar_TypeChecker_NBETerm.nbe_t with
- | FStar_TypeChecker_NBETerm.Meta (t, tm) ->
- let uu___1 = FStar_Thunk.force tm in
- (match uu___1 with
- | FStar_Syntax_Syntax.Meta_desugared m ->
- (t, (FStar_Pervasives_Native.Some m))
- | uu___2 -> (a, FStar_Pervasives_Native.None))
- | uu___1 -> (a, FStar_Pervasives_Native.None) in
- match uu___ with
- | (a1, m) ->
- (match a1.FStar_TypeChecker_NBETerm.nbe_t with
- | FStar_TypeChecker_NBETerm.FV (fv1, [], (a2, uu___1)::[])
- when
- let uu___2 = int_to_t_lid_for k in
- FStar_Ident.lid_equals
- (fv1.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v
- uu___2
- ->
- Obj.magic
- (Obj.repr
- (let uu___2 =
- FStar_TypeChecker_NBETerm.unembed
- FStar_TypeChecker_NBETerm.e_int cbs a2 in
- FStar_Class_Monad.op_let_Bang
- FStar_Class_Monad.monad_option () ()
- (Obj.magic uu___2)
- (fun uu___3 ->
- (fun a3 ->
- let a3 = Obj.magic a3 in
- Obj.magic
- (FStar_Pervasives_Native.Some
- (Mk (a3, m)))) uu___3)))
- | uu___1 -> Obj.magic (Obj.repr FStar_Pervasives_Native.None)))
- uu___1 uu___ in
+ let uu___2 = FStar_BigInt.string_of_big_int i in
+ let uu___3 =
+ let uu___4 =
+ let uu___5 = signedness k in
+ let uu___6 = width k in (uu___5, uu___6) in
+ FStar_Pervasives_Native.Some uu___4 in
+ (uu___2, uu___3) in
+ FStar_Const.Const_int uu___1 in
+ FStar_TypeChecker_NBETerm.mk_t
+ (FStar_TypeChecker_NBETerm.Constant
+ (FStar_TypeChecker_NBETerm.SConst const)) in
+ let un cbs a =
+ match a.FStar_TypeChecker_NBETerm.nbe_t with
+ | FStar_TypeChecker_NBETerm.Constant (FStar_TypeChecker_NBETerm.SConst
+ (FStar_Const.Const_int (str, FStar_Pervasives_Native.Some (s, w))))
+ when
+ (let uu___ = signedness k in s = uu___) &&
+ (let uu___ = width k in w = uu___)
+ ->
+ let n = FStar_BigInt.big_int_of_string str in
+ FStar_Pervasives_Native.Some (Mk n)
+ | uu___ -> FStar_Pervasives_Native.None in
FStar_TypeChecker_NBETerm.mk_emb em un
(fun uu___ ->
let uu___1 =
diff --git a/ocaml/fstar-lib/generated/FStar_Const.ml b/ocaml/fstar-lib/generated/FStar_Const.ml
index cfd47dcfa18..373091be07f 100644
--- a/ocaml/fstar-lib/generated/FStar_Const.ml
+++ b/ocaml/fstar-lib/generated/FStar_Const.ml
@@ -11,7 +11,8 @@ type width =
| Int16
| Int32
| Int64
- | Sizet [@@deriving yojson,show]
+ | Sizet
+ | Int128 [@@deriving yojson,show]
let (uu___is_Int8 : width -> Prims.bool) =
fun projectee -> match projectee with | Int8 -> true | uu___ -> false
let (uu___is_Int16 : width -> Prims.bool) =
@@ -22,6 +23,8 @@ let (uu___is_Int64 : width -> Prims.bool) =
fun projectee -> match projectee with | Int64 -> true | uu___ -> false
let (uu___is_Sizet : width -> Prims.bool) =
fun projectee -> match projectee with | Sizet -> true | uu___ -> false
+let (uu___is_Int128 : width -> Prims.bool) =
+ fun projectee -> match projectee with | Int128 -> true | uu___ -> false
type sconst =
| Const_effect
| Const_unit
@@ -122,7 +125,8 @@ let (bounds :
| Int16 -> FStar_BigInt.big_int_of_string "16"
| Int32 -> FStar_BigInt.big_int_of_string "32"
| Int64 -> FStar_BigInt.big_int_of_string "64"
- | Sizet -> FStar_BigInt.big_int_of_string "16" in
+ | Sizet -> FStar_BigInt.big_int_of_string "16"
+ | Int128 -> FStar_BigInt.big_int_of_string "128" in
let uu___ =
match signedness1 with
| Unsigned ->
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml
index 7fcfd765d0f..c5143ae8fd4 100644
--- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml
+++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml
@@ -1566,30 +1566,18 @@ let rec (extract_one_pat :
let uu___ = FStar_Options.codegen () in
uu___ <> (FStar_Pervasives_Native.Some FStar_Options.Krml) ->
let uu___ =
- match swopt with
- | FStar_Pervasives_Native.None ->
- let uu___1 =
- let uu___2 =
- let uu___3 =
- FStar_Extraction_ML_Util.mlconst_of_const
- p.FStar_Syntax_Syntax.p
- (FStar_Const.Const_int
- (c, FStar_Pervasives_Native.None)) in
- FStar_Extraction_ML_Syntax.MLE_Const uu___3 in
- FStar_Extraction_ML_Syntax.with_ty
- FStar_Extraction_ML_Syntax.ml_int_ty uu___2 in
- (uu___1, FStar_Extraction_ML_Syntax.ml_int_ty)
- | FStar_Pervasives_Native.Some sw ->
- let source_term =
- let uu___1 =
- let uu___2 =
- FStar_Extraction_ML_UEnv.tcenv_of_uenv g in
- uu___2.FStar_TypeChecker_Env.dsenv in
- FStar_ToSyntax_ToSyntax.desugar_machine_integer
- uu___1 c sw FStar_Compiler_Range_Type.dummyRange in
- let uu___1 = term_as_mlexpr g source_term in
- (match uu___1 with
- | (mlterm, uu___2, mlty) -> (mlterm, mlty)) in
+ let cc = FStar_Const.Const_int (c, swopt) in
+ let ty =
+ let uu___1 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in
+ FStar_TypeChecker_TcTerm.tc_constant uu___1
+ p.FStar_Syntax_Syntax.p cc in
+ let ml_ty = term_as_mlty g ty in
+ let uu___1 =
+ let uu___2 =
+ FStar_Extraction_ML_Util.mlexpr_of_const
+ p.FStar_Syntax_Syntax.p cc in
+ FStar_Extraction_ML_Syntax.with_ty ml_ty uu___2 in
+ (uu___1, ml_ty) in
(match uu___ with
| (mlc, ml_ty) ->
let uu___1 = FStar_Extraction_ML_UEnv.new_mlident g in
@@ -2622,6 +2610,29 @@ and (term_as_mlexpr :
| (e1, f, t) ->
let uu___1 = maybe_promote_effect e1 f t in
(match uu___1 with | (e2, f1) -> (e2, f1, t))
+and (mlexpr_of_const' :
+ FStar_Extraction_ML_UEnv.uenv ->
+ FStar_Compiler_Range_Type.range ->
+ FStar_Syntax_Syntax.sconst -> FStar_Extraction_ML_Syntax.mlexpr')
+ =
+ fun g ->
+ fun p ->
+ fun c ->
+ match c with
+ | FStar_Const.Const_int
+ (s, FStar_Pervasives_Native.Some
+ (FStar_Const.Unsigned, FStar_Const.Int128))
+ ->
+ let tm =
+ let uu___ =
+ let uu___1 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in
+ uu___1.FStar_TypeChecker_Env.dsenv in
+ FStar_ToSyntax_ToSyntax.unfold_machine_integer uu___ s
+ (FStar_Const.Unsigned, FStar_Const.Int128) p in
+ let uu___ = term_as_mlexpr' g tm in
+ (match uu___ with
+ | (mle, uu___1, uu___2) -> mle.FStar_Extraction_ML_Syntax.expr)
+ | uu___ -> FStar_Extraction_ML_Util.mlexpr_of_const p c
and (term_as_mlexpr' :
FStar_Extraction_ML_UEnv.uenv ->
FStar_Syntax_Syntax.term ->
@@ -2876,43 +2887,6 @@ and (term_as_mlexpr' :
(FStar_Extraction_ML_Syntax.ml_unit,
FStar_Extraction_ML_Syntax.E_ERASABLE,
FStar_Extraction_ML_Syntax.MLTY_Erased)
- | FStar_Syntax_Syntax.Tm_meta
- { FStar_Syntax_Syntax.tm2 = t1;
- FStar_Syntax_Syntax.meta = FStar_Syntax_Syntax.Meta_desugared
- (FStar_Syntax_Syntax.Machine_integer (signedness, width));_}
- ->
- let t2 = FStar_Syntax_Subst.compress t1 in
- let t3 = FStar_Syntax_Util.unascribe t2 in
- (match t3.FStar_Syntax_Syntax.n with
- | FStar_Syntax_Syntax.Tm_app
- { FStar_Syntax_Syntax.hd = hd;
- FStar_Syntax_Syntax.args = (x, uu___1)::[];_}
- ->
- let x1 = FStar_Syntax_Subst.compress x in
- let x2 = FStar_Syntax_Util.unascribe x1 in
- (match x2.FStar_Syntax_Syntax.n with
- | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_int
- (repr, uu___2)) ->
- let uu___3 =
- let uu___4 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in
- FStar_TypeChecker_TcTerm.typeof_tot_or_gtot_term
- uu___4 t3 true in
- (match uu___3 with
- | (uu___4, ty, uu___5) ->
- let ml_ty = term_as_mlty g ty in
- let ml_const =
- FStar_Const.Const_int
- (repr,
- (FStar_Pervasives_Native.Some
- (signedness, width))) in
- let uu___6 =
- let uu___7 =
- FStar_Extraction_ML_Util.mlexpr_of_const
- t3.FStar_Syntax_Syntax.pos ml_const in
- FStar_Extraction_ML_Syntax.with_ty ml_ty uu___7 in
- (uu___6, FStar_Extraction_ML_Syntax.E_PURE, ml_ty))
- | uu___2 -> term_as_mlexpr g t3)
- | uu___1 -> term_as_mlexpr g t3)
| FStar_Syntax_Syntax.Tm_meta
{ FStar_Syntax_Syntax.tm2 = t1;
FStar_Syntax_Syntax.meta = uu___1;_}
@@ -2926,9 +2900,7 @@ and (term_as_mlexpr' :
| (uu___2, ty, uu___3) ->
let ml_ty = term_as_mlty g ty in
let uu___4 =
- let uu___5 =
- FStar_Extraction_ML_Util.mlexpr_of_const
- t.FStar_Syntax_Syntax.pos c in
+ let uu___5 = mlexpr_of_const' g t.FStar_Syntax_Syntax.pos c in
FStar_Extraction_ML_Syntax.with_ty ml_ty uu___5 in
(uu___4, FStar_Extraction_ML_Syntax.E_PURE, ml_ty))
| FStar_Syntax_Syntax.Tm_name uu___1 ->
diff --git a/ocaml/fstar-lib/generated/FStar_Int128.ml b/ocaml/fstar-lib/generated/FStar_Int128.ml
index 8f6fabf749a..09cb555122c 100644
--- a/ocaml/fstar-lib/generated/FStar_Int128.ml
+++ b/ocaml/fstar-lib/generated/FStar_Int128.ml
@@ -71,8 +71,7 @@ let (op_Less_Hat : t -> t -> Prims.bool) = lt
let (op_Less_Equals_Hat : t -> t -> Prims.bool) = lte
let (ct_abs : t -> t) =
fun a ->
- let mask =
- shift_arithmetic_right a (FStar_UInt32.uint_to_t (Prims.of_int (127))) in
+ let mask = shift_arithmetic_right a (Stdint.Uint32.of_int (127)) in
sub (logxor a mask) mask
let (to_string : t -> Prims.string) = fun uu___ -> Prims.admit ()
let (of_string : Prims.string -> t) = fun uu___ -> Prims.admit ()
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
index 86a9f8374df..1a07c59447e 100644
--- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
+++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
@@ -48,6 +48,7 @@ let (int32_lid : FStar_Ident.lident) = p2l ["FStar"; "Int32"; "t"]
let (uint32_lid : FStar_Ident.lident) = p2l ["FStar"; "UInt32"; "t"]
let (int64_lid : FStar_Ident.lident) = p2l ["FStar"; "Int64"; "t"]
let (uint64_lid : FStar_Ident.lident) = p2l ["FStar"; "UInt64"; "t"]
+let (uint128_lid : FStar_Ident.lident) = p2l ["FStar"; "UInt128"; "t"]
let (sizet_lid : FStar_Ident.lident) = p2l ["FStar"; "SizeT"; "t"]
let (salloc_lid : FStar_Ident.lident) = p2l ["FStar"; "ST"; "salloc"]
let (swrite_lid : FStar_Ident.lident) =
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml
index 5f77a02095f..3dd59923df0 100644
--- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml
+++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml
@@ -683,7 +683,7 @@ let rec (encode_const :
(uu___1, [])
| FStar_Const.Const_int (repr, FStar_Pervasives_Native.Some sw) ->
let syntax_term =
- FStar_ToSyntax_ToSyntax.desugar_machine_integer
+ FStar_ToSyntax_ToSyntax.unfold_machine_integer
(env.FStar_SMTEncoding_Env.tcenv).FStar_TypeChecker_Env.dsenv
repr sw FStar_Compiler_Range_Type.dummyRange in
encode_term syntax_term env
diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
index 70c5bc1635d..cab2360f2a2 100644
--- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
@@ -2321,10 +2321,11 @@ and (desugar_typ :
let uu___ = desugar_typ_aq env e in
match uu___ with | (t, aq) -> (check_no_aq aq; t)
and (desugar_machine_integer :
- FStar_Syntax_DsEnv.env ->
+ env_t ->
Prims.string ->
(FStar_Const.signedness * FStar_Const.width) ->
- FStar_Compiler_Range_Type.range -> FStar_Syntax_Syntax.term)
+ FStar_Compiler_Range_Type.range ->
+ FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax)
=
fun env ->
fun repr ->
@@ -2346,7 +2347,8 @@ and (desugar_machine_integer :
| FStar_Const.Int8 -> "8"
| FStar_Const.Int16 -> "16"
| FStar_Const.Int32 -> "32"
- | FStar_Const.Int64 -> "64"))) in
+ | FStar_Const.Int64 -> "64"
+ | FStar_Const.Int128 -> "128"))) in
((let uu___2 =
let uu___3 =
FStar_Const.within_bounds repr signedness width in
@@ -2360,92 +2362,12 @@ and (desugar_machine_integer :
(FStar_Errors_Codes.Error_OutOfRange, uu___4) in
FStar_Errors.log_issue range uu___3
else ());
- (let private_intro_nm =
- Prims.strcat tnm
- (Prims.strcat ".__"
- (Prims.strcat
- (match signedness with
- | FStar_Const.Unsigned -> "u"
- | FStar_Const.Signed -> "") "int_to_t")) in
- let intro_nm =
- Prims.strcat tnm
- (Prims.strcat "."
- (Prims.strcat
- (match signedness with
- | FStar_Const.Unsigned -> "u"
- | FStar_Const.Signed -> "") "int_to_t")) in
- let lid =
- let uu___2 = FStar_Ident.path_of_text intro_nm in
- FStar_Ident.lid_of_path uu___2 range in
- let lid1 =
- let uu___2 = FStar_Syntax_DsEnv.try_lookup_lid env lid in
- match uu___2 with
- | FStar_Pervasives_Native.Some intro_term ->
- (match intro_term.FStar_Syntax_Syntax.n with
- | FStar_Syntax_Syntax.Tm_fvar fv ->
- let private_lid =
- let uu___3 =
- FStar_Ident.path_of_text private_intro_nm in
- FStar_Ident.lid_of_path uu___3 range in
- let private_fv =
- let uu___3 =
- FStar_Syntax_Util.incr_delta_depth
- (FStar_Pervasives_Native.__proj__Some__item__v
- fv.FStar_Syntax_Syntax.fv_delta) in
- FStar_Syntax_Syntax.lid_and_dd_as_fv private_lid
- uu___3 fv.FStar_Syntax_Syntax.fv_qual in
- {
- FStar_Syntax_Syntax.n =
- (FStar_Syntax_Syntax.Tm_fvar private_fv);
- FStar_Syntax_Syntax.pos =
- (intro_term.FStar_Syntax_Syntax.pos);
- FStar_Syntax_Syntax.vars =
- (intro_term.FStar_Syntax_Syntax.vars);
- FStar_Syntax_Syntax.hash_code =
- (intro_term.FStar_Syntax_Syntax.hash_code)
- }
- | uu___3 ->
- FStar_Compiler_Effect.failwith
- (Prims.strcat "Unexpected non-fvar for "
- intro_nm))
- | FStar_Pervasives_Native.None ->
- let uu___3 =
- let uu___4 =
- FStar_Compiler_Util.format1
- "Unexpected numeric literal. Restart F* to load %s."
- tnm in
- (FStar_Errors_Codes.Fatal_UnexpectedNumericLiteral,
- uu___4) in
- FStar_Errors.raise_error uu___3 range in
- let repr' =
- FStar_Syntax_Syntax.mk
- (FStar_Syntax_Syntax.Tm_constant
- (FStar_Const.Const_int
- (repr, FStar_Pervasives_Native.None))) range in
- let app =
- let uu___2 =
- let uu___3 =
- let uu___4 =
- let uu___5 =
- let uu___6 =
- FStar_Syntax_Syntax.as_aqual_implicit false in
- (repr', uu___6) in
- [uu___5] in
- {
- FStar_Syntax_Syntax.hd = lid1;
- FStar_Syntax_Syntax.args = uu___4
- } in
- FStar_Syntax_Syntax.Tm_app uu___3 in
- FStar_Syntax_Syntax.mk uu___2 range in
- FStar_Syntax_Syntax.mk
- (FStar_Syntax_Syntax.Tm_meta
- {
- FStar_Syntax_Syntax.tm2 = app;
- FStar_Syntax_Syntax.meta =
- (FStar_Syntax_Syntax.Meta_desugared
- (FStar_Syntax_Syntax.Machine_integer
- (signedness, width)))
- }) range))
+ (let c =
+ FStar_Const.Const_int
+ (repr,
+ (FStar_Pervasives_Native.Some (signedness, width))) in
+ FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_constant c)
+ range))
and (desugar_term_maybe_top :
Prims.bool ->
env_t ->
@@ -10402,4 +10324,84 @@ let (add_modul_to_env :
FStar_Syntax_DsEnv.module_inclusion_info ->
(FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) ->
unit FStar_Syntax_DsEnv.withenv)
- = add_modul_to_env_core true
\ No newline at end of file
+ = add_modul_to_env_core true
+let (unfold_machine_integer :
+ FStar_Syntax_DsEnv.env ->
+ Prims.string ->
+ (FStar_Const.signedness * FStar_Const.width) ->
+ FStar_Compiler_Range_Type.range -> FStar_Syntax_Syntax.term)
+ =
+ fun env ->
+ fun repr ->
+ fun uu___ ->
+ fun range ->
+ match uu___ with
+ | (signedness, width) ->
+ let tnm =
+ if width = FStar_Const.Sizet
+ then "FStar.SizeT"
+ else
+ Prims.strcat "FStar."
+ (Prims.strcat
+ (match signedness with
+ | FStar_Const.Unsigned -> "U"
+ | FStar_Const.Signed -> "")
+ (Prims.strcat "Int"
+ (match width with
+ | FStar_Const.Int8 -> "8"
+ | FStar_Const.Int16 -> "16"
+ | FStar_Const.Int32 -> "32"
+ | FStar_Const.Int64 -> "64"
+ | FStar_Const.Int128 -> "128"))) in
+ let intro_nm =
+ Prims.strcat tnm
+ (Prims.strcat "."
+ (Prims.strcat
+ (match signedness with
+ | FStar_Const.Unsigned -> "u"
+ | FStar_Const.Signed -> "") "int_to_t")) in
+ let lid =
+ let uu___1 = FStar_Ident.path_of_text intro_nm in
+ FStar_Ident.lid_of_path uu___1 range in
+ let hd =
+ let uu___1 = FStar_Syntax_DsEnv.try_lookup_lid env lid in
+ match uu___1 with
+ | FStar_Pervasives_Native.Some intro_term -> intro_term
+ | FStar_Pervasives_Native.None ->
+ let uu___2 =
+ let uu___3 =
+ FStar_Compiler_Util.format1
+ "Unexpected numeric literal. Restart F* to load %s."
+ tnm in
+ (FStar_Errors_Codes.Fatal_UnexpectedNumericLiteral,
+ uu___3) in
+ FStar_Errors.raise_error uu___2 range in
+ let repr' =
+ FStar_Syntax_Syntax.mk
+ (FStar_Syntax_Syntax.Tm_constant
+ (FStar_Const.Const_int
+ (repr, FStar_Pervasives_Native.None))) range in
+ let app =
+ let uu___1 =
+ let uu___2 =
+ let uu___3 =
+ let uu___4 =
+ let uu___5 =
+ FStar_Syntax_Syntax.as_aqual_implicit false in
+ (repr', uu___5) in
+ [uu___4] in
+ {
+ FStar_Syntax_Syntax.hd = hd;
+ FStar_Syntax_Syntax.args = uu___3
+ } in
+ FStar_Syntax_Syntax.Tm_app uu___2 in
+ FStar_Syntax_Syntax.mk uu___1 range in
+ FStar_Syntax_Syntax.mk
+ (FStar_Syntax_Syntax.Tm_meta
+ {
+ FStar_Syntax_Syntax.tm2 = app;
+ FStar_Syntax_Syntax.meta =
+ (FStar_Syntax_Syntax.Meta_desugared
+ (FStar_Syntax_Syntax.Machine_integer
+ (signedness, width)))
+ }) range
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
index e2c80eed8dd..11468b68734 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
@@ -6668,7 +6668,7 @@ and (check_pat :
match c with
| FStar_Const.Const_int (repr, FStar_Pervasives_Native.Some sw)
->
- FStar_ToSyntax_ToSyntax.desugar_machine_integer
+ FStar_ToSyntax_ToSyntax.unfold_machine_integer
(g.tcenv).FStar_TypeChecker_Env.dsenv repr sw
p.FStar_Syntax_Syntax.p
| uu___ ->
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_PatternUtils.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_PatternUtils.ml
index 59d2cb75bff..ea1dfefdae6 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_PatternUtils.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_PatternUtils.ml
@@ -186,7 +186,7 @@ let (raw_pat_as_exp :
match c with
| FStar_Const.Const_int (repr, FStar_Pervasives_Native.Some sw)
->
- FStar_ToSyntax_ToSyntax.desugar_machine_integer
+ FStar_ToSyntax_ToSyntax.unfold_machine_integer
env.FStar_TypeChecker_Env.dsenv repr sw
p1.FStar_Syntax_Syntax.p
| uu___ ->
@@ -289,7 +289,7 @@ let (pat_as_exp :
match c with
| FStar_Const.Const_int
(repr, FStar_Pervasives_Native.Some sw) ->
- FStar_ToSyntax_ToSyntax.desugar_machine_integer
+ FStar_ToSyntax_ToSyntax.unfold_machine_integer
env1.FStar_TypeChecker_Env.dsenv repr sw
p1.FStar_Syntax_Syntax.p
| uu___ ->
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_MachineInts.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_MachineInts.ml
index 05fff5eef5a..b0353e6ee59 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_MachineInts.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_MachineInts.ml
@@ -24,24 +24,19 @@ let (bounded_arith_ops_for :
(FStar_Compiler_MachineInts.v k) in
let uu___3 =
let uu___4 =
- let uu___5 = nm "add" in
- FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero uu___5
+ let uu___5 =
+ let uu___6 =
+ let uu___7 = FStar_Compiler_MachineInts.is_unsigned k in
+ if uu___7 then "uint_to_t" else "int_to_t" in
+ nm uu___6 in
+ FStar_TypeChecker_Primops_Base.mk1 Prims.int_zero uu___5
+ FStar_Syntax_Embeddings.e_int FStar_TypeChecker_NBETerm.e_int
(FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
- (FStar_Compiler_MachineInts.e_machint k)
- (FStar_Compiler_MachineInts.nbe_machint k)
- (FStar_Compiler_MachineInts.e_machint k)
- (FStar_Compiler_MachineInts.nbe_machint k)
- (fun x ->
- fun y ->
- let uu___6 =
- let uu___7 = FStar_Compiler_MachineInts.v k x in
- let uu___8 = FStar_Compiler_MachineInts.v k y in
- FStar_BigInt.add_big_int uu___7 uu___8 in
- FStar_Compiler_MachineInts.make_as k x uu___6) in
+ (FStar_Compiler_MachineInts.int_to_t k) in
let uu___5 =
let uu___6 =
- let uu___7 = nm "sub" in
+ let uu___7 = nm "add" in
FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero uu___7
(FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
@@ -54,11 +49,11 @@ let (bounded_arith_ops_for :
let uu___8 =
let uu___9 = FStar_Compiler_MachineInts.v k x in
let uu___10 = FStar_Compiler_MachineInts.v k y in
- FStar_BigInt.sub_big_int uu___9 uu___10 in
+ FStar_BigInt.add_big_int uu___9 uu___10 in
FStar_Compiler_MachineInts.make_as k x uu___8) in
let uu___7 =
let uu___8 =
- let uu___9 = nm "mul" in
+ let uu___9 = nm "sub" in
FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero uu___9
(FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
@@ -71,26 +66,28 @@ let (bounded_arith_ops_for :
let uu___10 =
let uu___11 = FStar_Compiler_MachineInts.v k x in
let uu___12 = FStar_Compiler_MachineInts.v k y in
- FStar_BigInt.mult_big_int uu___11 uu___12 in
+ FStar_BigInt.sub_big_int uu___11 uu___12 in
FStar_Compiler_MachineInts.make_as k x uu___10) in
let uu___9 =
let uu___10 =
- let uu___11 = nm "gt" in
+ let uu___11 = nm "mul" in
FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero uu___11
(FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
(FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
- FStar_Syntax_Embeddings.e_bool
- FStar_TypeChecker_NBETerm.e_bool
+ (FStar_Compiler_MachineInts.e_machint k)
+ (FStar_Compiler_MachineInts.nbe_machint k)
(fun x ->
fun y ->
- let uu___12 = FStar_Compiler_MachineInts.v k x in
- let uu___13 = FStar_Compiler_MachineInts.v k y in
- FStar_BigInt.gt_big_int uu___12 uu___13) in
+ let uu___12 =
+ let uu___13 = FStar_Compiler_MachineInts.v k x in
+ let uu___14 = FStar_Compiler_MachineInts.v k y in
+ FStar_BigInt.mult_big_int uu___13 uu___14 in
+ FStar_Compiler_MachineInts.make_as k x uu___12) in
let uu___11 =
let uu___12 =
- let uu___13 = nm "gte" in
+ let uu___13 = nm "gt" in
FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero uu___13
(FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
@@ -102,10 +99,10 @@ let (bounded_arith_ops_for :
fun y ->
let uu___14 = FStar_Compiler_MachineInts.v k x in
let uu___15 = FStar_Compiler_MachineInts.v k y in
- FStar_BigInt.ge_big_int uu___14 uu___15) in
+ FStar_BigInt.gt_big_int uu___14 uu___15) in
let uu___13 =
let uu___14 =
- let uu___15 = nm "lt" in
+ let uu___15 = nm "gte" in
FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero
uu___15 (FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
@@ -117,10 +114,10 @@ let (bounded_arith_ops_for :
fun y ->
let uu___16 = FStar_Compiler_MachineInts.v k x in
let uu___17 = FStar_Compiler_MachineInts.v k y in
- FStar_BigInt.lt_big_int uu___16 uu___17) in
+ FStar_BigInt.ge_big_int uu___16 uu___17) in
let uu___15 =
let uu___16 =
- let uu___17 = nm "lte" in
+ let uu___17 = nm "lt" in
FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero
uu___17 (FStar_Compiler_MachineInts.e_machint k)
(FStar_Compiler_MachineInts.nbe_machint k)
@@ -132,8 +129,26 @@ let (bounded_arith_ops_for :
fun y ->
let uu___18 = FStar_Compiler_MachineInts.v k x in
let uu___19 = FStar_Compiler_MachineInts.v k y in
- FStar_BigInt.le_big_int uu___18 uu___19) in
- [uu___16] in
+ FStar_BigInt.lt_big_int uu___18 uu___19) in
+ let uu___17 =
+ let uu___18 =
+ let uu___19 = nm "lte" in
+ FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero
+ uu___19 (FStar_Compiler_MachineInts.e_machint k)
+ (FStar_Compiler_MachineInts.nbe_machint k)
+ (FStar_Compiler_MachineInts.e_machint k)
+ (FStar_Compiler_MachineInts.nbe_machint k)
+ FStar_Syntax_Embeddings.e_bool
+ FStar_TypeChecker_NBETerm.e_bool
+ (fun x ->
+ fun y ->
+ let uu___20 =
+ FStar_Compiler_MachineInts.v k x in
+ let uu___21 =
+ FStar_Compiler_MachineInts.v k y in
+ FStar_BigInt.le_big_int uu___20 uu___21) in
+ [uu___18] in
+ uu___16 :: uu___17 in
uu___14 :: uu___15 in
uu___12 :: uu___13 in
uu___10 :: uu___11 in
@@ -148,7 +163,7 @@ let (bounded_arith_ops_for :
(fun uu___1 ->
(fun uu___1 ->
let uu___1 = Obj.magic uu___1 in
- let sz = FStar_Compiler_MachineInts.width k in
+ let sz = FStar_Compiler_MachineInts.widthn k in
let modulus =
let uu___2 = FStar_BigInt.of_int_fs sz in
FStar_BigInt.shift_left_big_int FStar_BigInt.one uu___2 in
@@ -624,8 +639,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) =
FStar_BigInt.of_int_fs
(FStar_Compiler_Util.int_of_char c) in
FStar_Compiler_MachineInts.mk
- FStar_Compiler_MachineInts.UInt32 n
- FStar_Pervasives_Native.None) in
+ FStar_Compiler_MachineInts.UInt32 n) in
[uu___5] in
Obj.magic
(FStar_Compiler_Writer.emit
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
index 4d416a1b54f..09a434d9c86 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
@@ -4877,6 +4877,8 @@ and (tc_constant :
FStar_Parser_Const.uint32_lid
| (FStar_Const.Unsigned, FStar_Const.Int64) ->
FStar_Parser_Const.uint64_lid
+ | (FStar_Const.Unsigned, FStar_Const.Int128) ->
+ FStar_Parser_Const.uint128_lid
| (FStar_Const.Unsigned, FStar_Const.Sizet) ->
FStar_Parser_Const.sizet_lid)
| FStar_Const.Const_string uu___ -> FStar_Syntax_Syntax.t_string
diff --git a/ocaml/fstar-lib/generated/FStar_UInt128.ml b/ocaml/fstar-lib/generated/FStar_UInt128.ml
index c1da8cedf7c..88fca4a7538 100644
--- a/ocaml/fstar-lib/generated/FStar_UInt128.ml
+++ b/ocaml/fstar-lib/generated/FStar_UInt128.ml
@@ -124,7 +124,7 @@ let (lognot : t -> t) =
{ low = (FStar_UInt64.lognot a.low); high = (FStar_UInt64.lognot a.high)
}
let (__uint_to_t : Prims.int -> t) = fun x -> uint_to_t x
-let (u32_64 : FStar_UInt32.t) = FStar_UInt32.uint_to_t (Prims.of_int (64))
+let (u32_64 : FStar_UInt32.t) = (Stdint.Uint32.of_int (64))
let (add_u64_shift_left :
FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt32.t -> FStar_UInt64.t) =
fun hi ->
@@ -149,7 +149,7 @@ let (shift_left_large : t -> FStar_UInt32.t -> t) =
fun a ->
fun s ->
{
- low = (FStar_UInt64.uint_to_t Prims.int_zero);
+ low = Stdint.Uint64.zero;
high = (FStar_UInt64.shift_left a.low (FStar_UInt32.sub s u32_64))
}
let (shift_left : t -> FStar_UInt32.t -> t) =
@@ -183,7 +183,7 @@ let (shift_right_large : t -> FStar_UInt32.t -> t) =
fun s ->
{
low = (FStar_UInt64.shift_right a.high (FStar_UInt32.sub s u32_64));
- high = (FStar_UInt64.uint_to_t Prims.int_zero)
+ high = Stdint.Uint64.zero
}
let (shift_right : t -> FStar_UInt32.t -> t) =
fun a ->
@@ -243,15 +243,12 @@ let (gte_mask : t -> t -> t) =
(FStar_UInt64.gte_mask a.low b.low)))
}
let (uint64_to_uint128 : FStar_UInt64.t -> t) =
- fun a -> { low = a; high = (FStar_UInt64.uint_to_t Prims.int_zero) }
+ fun a -> { low = a; high = Stdint.Uint64.zero }
let (uint128_to_uint64 : t -> FStar_UInt64.t) = fun a -> a.low
-let (u64_l32_mask : FStar_UInt64.t) =
- FStar_UInt64.uint_to_t (Prims.parse_int "0xffffffff")
+let (u64_l32_mask : FStar_UInt64.t) = (Stdint.Uint64.of_string "4294967295")
let (u64_mod_32 : FStar_UInt64.t -> FStar_UInt64.t) =
- fun a ->
- FStar_UInt64.logand a
- (FStar_UInt64.uint_to_t (Prims.parse_int "0xffffffff"))
-let (u32_32 : FStar_UInt32.t) = FStar_UInt32.uint_to_t (Prims.of_int (32))
+ fun a -> FStar_UInt64.logand a (Stdint.Uint64.of_string "4294967295")
+let (u32_32 : FStar_UInt32.t) = (Stdint.Uint32.of_int (32))
let (u32_combine : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt64.t) =
fun hi -> fun lo -> FStar_UInt64.add lo (FStar_UInt64.shift_left hi u32_32)
let (mul32 : FStar_UInt64.t -> FStar_UInt32.t -> t) =
diff --git a/src/basic/FStar.Compiler.MachineInts.fst b/src/basic/FStar.Compiler.MachineInts.fst
index a0ea37f5a46..4f0cdebe154 100644
--- a/src/basic/FStar.Compiler.MachineInts.fst
+++ b/src/basic/FStar.Compiler.MachineInts.fst
@@ -36,7 +36,7 @@ let is_unsigned (k : machint_kind) : bool =
| SizeT -> true
let is_signed k = not (is_unsigned k)
-let width (k : machint_kind) : int =
+let widthn (k : machint_kind) : int =
match k with
| Int8 -> 8
| Int16 -> 16
@@ -63,43 +63,41 @@ let module_name_for (k:machint_kind) : string =
| SizeT -> "SizeT"
let mask (k:machint_kind) : Z.t =
- match width k with
+ match widthn k with
| 8 -> Z.of_hex "ff"
| 16 -> Z.of_hex "ffff"
| 32 -> Z.of_hex "ffffffff"
| 64 -> Z.of_hex "ffffffffffffffff"
| 128 -> Z.of_hex "ffffffffffffffffffffffffffffffff"
-let int_to_t_lid_for (k:machint_kind) : Ident.lid =
- let path = "FStar" :: module_name_for k :: (if is_unsigned k then "uint_to_t" else "int_to_t") :: [] in
- Ident.lid_of_path path Range.dummyRange
+let signedness (k:machint_kind) : Const.signedness =
+ if is_unsigned k then Const.Unsigned else Const.Signed
-let int_to_t_for (k:machint_kind) : S.term =
- let lid = int_to_t_lid_for k in
- S.fvar lid None
-
-let __int_to_t_lid_for (k:machint_kind) : Ident.lid =
- let path = "FStar" :: module_name_for k :: (if is_unsigned k then "__uint_to_t" else "__int_to_t") :: [] in
- Ident.lid_of_path path Range.dummyRange
-
-let __int_to_t_for (k:machint_kind) : S.term =
- let lid = __int_to_t_lid_for k in
- S.fvar lid None
+let width (k:machint_kind) : Const.width =
+ match k with
+ | Int8 | UInt8 -> Const.Int8
+ | Int16 | UInt16 -> Const.Int16
+ | Int32 | UInt32 -> Const.Int32
+ | Int64 | UInt64 -> Const.Int64
+ | UInt128 -> Const.Int128
+ | SizeT -> Const.Sizet
(* just a newtype really, no checks or conditions here *)
-type machint (k : machint_kind) = | Mk : Z.t -> option S.meta_source_info -> machint k
+type machint (k : machint_kind) = | Mk : Z.t -> machint k
-let mk #k x m = Mk #k x m
+let mk #k x = Mk #k x
let v #k (x : machint k) =
- let Mk v _ = x in v
-let meta #k (x : machint k) =
- let Mk _ meta = x in meta
+ let Mk v = x in v
+let int_to_t #k (i : Z.t) : machint k =
+ (* FIXME: Check bounds? *)
+ Mk i
+
let make_as #k (x : machint k) (z : Z.t) : machint k =
- Mk z (meta x)
+ Mk z
(* just for debugging *)
instance showable_bounded_k k : Tot (showable (machint k)) = {
- show = (function Mk x m -> "machine integer " ^ show (Z.to_int_fs x) ^ "@@" ^ module_name_for k);
+ show = (function Mk x -> "machine integer " ^ show (Z.to_int_fs x) ^ "@@" ^ module_name_for k);
}
instance e_machint (k : machint_kind) : Tot (EMB.embedding (machint k)) =
@@ -109,25 +107,17 @@ instance e_machint (k : machint_kind) : Tot (EMB.embedding (machint k)) =
| Some m -> S.mk (Tm_meta {tm=t; meta=Meta_desugared m}) r
in
let em (x : machint k) rng shadow cb =
- let Mk i m = x in
- let it = EMB.embed i rng None cb in
- let int_to_t = int_to_t_for k in
- let t = S.mk_Tm_app int_to_t [S.as_arg it] rng in
- with_meta_ds rng t m
+ let Mk i = x in
+ let const = Const.Const_int (Z.string_of_big_int i, Some (signedness k, width k)) in
+ S.mk (S.Tm_constant const) rng
in
let un (t:term) cb : option (machint k) =
- let (t, m) =
- (match (SS.compress t).n with
- | Tm_meta {tm=t; meta=Meta_desugared m} -> (t, Some m)
- | _ -> (t, None))
- in
let t = U.unmeta_safe t in
match (SS.compress t).n with
- | Tm_app {hd; args=[(a,_)]} when U.is_fvar (int_to_t_lid_for k) hd
- || U.is_fvar (__int_to_t_lid_for k) hd ->
- let a = U.unlazy_emb a in
- let! a : Z.t = EMB.try_unembed a cb in
- Some (Mk a m)
+ | Tm_constant (Const.Const_int (str, Some (s, w)))
+ when s = signedness k && w = width k ->
+ let n = Z.big_int_of_string str in
+ Some (Mk n)
| _ ->
None
in
@@ -143,29 +133,19 @@ instance nbe_machint (k : machint_kind) : Tot (NBE.embedding (machint k)) =
| None -> t
| Some m -> NBE.mk_t (Meta(t, Thunk.mk (fun _ -> Meta_desugared m)))
in
- let em cbs (x : machint k) =
- let Mk i m = x in
- let it = embed e_int cbs i in
- let int_to_t args = mk_t <| FV (S.lid_as_fv (__int_to_t_lid_for k) None, [], args) in
- let t = int_to_t [as_arg it] in
- with_meta_ds t m
+ let em cbs (x : machint k) : t =
+ let Mk i = x in
+ let const = Const.Const_int (Z.string_of_big_int i, Some (signedness k, width k)) in
+ mk_t <| Constant (SConst const)
in
let un cbs a : option (machint k) =
- let (a, m) =
- (match a.nbe_t with
- | Meta(t, tm) ->
- (match Thunk.force tm with
- | Meta_desugared m -> (t, Some m)
- | _ -> (a, None))
- | _ -> (a, None))
- in
match a.nbe_t with
- | FV (fv1, [], [(a, _)]) when Ident.lid_equals (fv1.fv_name.v) (int_to_t_lid_for k) ->
- let! a : Z.t = unembed e_int cbs a in
- Some (Mk a m)
+ | Constant (SConst (Const.Const_int (str, Some (s, w))))
+ when s = signedness k && w = width k ->
+ let n = Z.big_int_of_string str in
+ Some (Mk n)
| _ -> None
in
mk_emb em un
(fun () -> mkFV (lid_as_fv (Ident.lid_of_path ["FStar"; module_name_for k; "t"] Range.dummyRange) None) [] [])
(fun () -> ET_abstract)
-
diff --git a/src/basic/FStar.Compiler.MachineInts.fsti b/src/basic/FStar.Compiler.MachineInts.fsti
index 2f07bb7b1c1..3b80ead20e0 100644
--- a/src/basic/FStar.Compiler.MachineInts.fsti
+++ b/src/basic/FStar.Compiler.MachineInts.fsti
@@ -27,15 +27,15 @@ val all_machint_kinds : list machint_kind
val is_unsigned (k : machint_kind) : bool
val is_signed (k : machint_kind) : bool
-val width (k : machint_kind) : int
+val widthn (k : machint_kind) : int
val module_name_for (k:machint_kind) : string
val mask (k:machint_kind) : Z.t
new val machint (k : machint_kind) : Type0
-val mk (#k:_) (i : Z.t) (m : option S.meta_source_info) : machint k // no checks at all, use with care
+val mk (#k:_) (i : Z.t) : machint k // no checks at all, use with care
val v #k (x : machint k) : Z.t
-val meta #k (x : machint k) : option S.meta_source_info
+val int_to_t #k (i : Z.t) : machint k
(* Make a machint k copying the meta off an existing one *)
val make_as #k (x : machint k) (z : Z.t) : machint k
diff --git a/src/basic/FStar.Const.fst b/src/basic/FStar.Const.fst
index 7b016a267b5..6f764b38006 100644
--- a/src/basic/FStar.Const.fst
+++ b/src/basic/FStar.Const.fst
@@ -22,7 +22,7 @@ open FStar.BaseTypes
[@@ PpxDerivingYoJson; PpxDerivingShow ]
type signedness = | Unsigned | Signed
[@@ PpxDerivingYoJson; PpxDerivingShow ]
-type width = | Int8 | Int16 | Int32 | Int64 | Sizet
+type width = | Int8 | Int16 | Int32 | Int64 | Sizet | Int128
(* NB:
Const_int (_, None) is not a canonical representation for a mathematical integer
@@ -78,6 +78,7 @@ let bounds signedness width =
| Int32 -> big_int_of_string "32"
| Int64 -> big_int_of_string "64"
| Sizet -> big_int_of_string "16"
+ | Int128 -> big_int_of_string "128"
in
let lower, upper =
match signedness with
diff --git a/src/extraction/FStar.Extraction.ML.Term.fst b/src/extraction/FStar.Extraction.ML.Term.fst
index 72df6af7cd0..ee63e5307ac 100644
--- a/src/extraction/FStar.Extraction.ML.Term.fst
+++ b/src/extraction/FStar.Extraction.ML.Term.fst
@@ -952,15 +952,10 @@ let rec extract_one_pat (imp : bool)
//Karamel supports native integer constants in patterns
//Don't convert them into `when` clauses
let mlc, ml_ty =
- match swopt with
- | None ->
- with_ty ml_int_ty <| (MLE_Const (mlconst_of_const p.p (Const_int (c, None)))),
- ml_int_ty
- | Some sw ->
- let source_term =
- FStar.ToSyntax.ToSyntax.desugar_machine_integer (tcenv_of_uenv g).dsenv c sw Range.dummyRange in
- let mlterm, _, mlty = term_as_mlexpr g source_term in
- mlterm, mlty
+ let cc = Const_int (c, swopt) in
+ let ty = TcTerm.tc_constant (tcenv_of_uenv g) p.p cc in
+ let ml_ty = term_as_mlty g ty in
+ with_ty ml_ty (mlexpr_of_const p.p cc), ml_ty
in
//these may be extracted to bigint, in which case, we need to emit a when clause
let g, x = UEnv.new_mlident g in
@@ -1349,6 +1344,16 @@ and term_as_mlexpr (g:uenv) (e:term) : (mlexpr * e_tag * mlty) =
e, f, t
+and mlexpr_of_const' (g:uenv) (p:Range.range) (c:sconst) : mlexpr' =
+ (* As mlexpr_of_const, but handles UInt128 *)
+ match c with
+ | Const_int (s, Some (Unsigned, Int128)) ->
+ let tm = FStar.ToSyntax.ToSyntax.unfold_machine_integer (tcenv_of_uenv g).dsenv s (Unsigned, Int128) p in
+ let mle, _, _ = term_as_mlexpr' g tm in
+ mle.expr
+
+ | _ -> mlexpr_of_const p c
+
and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr * e_tag * mlty) =
let top = SS.compress top in
(debug g (fun u -> BU.print_string (BU.format3 "%s: term_as_mlexpr' (%s) : %s \n"
@@ -1463,25 +1468,6 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr * e_tag * mlty) =
*)
ml_unit, E_ERASABLE, MLTY_Erased
- | Tm_meta {tm=t; meta=Meta_desugared (Machine_integer (signedness, width))} ->
-
- let t = SS.compress t in
- let t = U.unascribe t in
- (match t.n with
- (* Should we check if hd here is [__][u]int_to_t? *)
- | Tm_app {hd; args=[x, _]} ->
- (let x = SS.compress x in
- let x = U.unascribe x in
- match x.n with
- | Tm_constant (Const_int (repr, _)) ->
- (let _, ty, _ =
- TcTerm.typeof_tot_or_gtot_term (tcenv_of_uenv g) t true in
- let ml_ty = term_as_mlty g ty in
- let ml_const = Const_int (repr, Some (signedness, width)) in
- with_ty ml_ty (mlexpr_of_const t.pos ml_const), E_PURE, ml_ty)
- |_ -> term_as_mlexpr g t)
- | _ -> term_as_mlexpr g t)
-
| Tm_meta {tm=t} //TODO: handle the resugaring in case it's a 'Meta_desugared' ... for more readable output
| Tm_uinst(t, _) ->
term_as_mlexpr g t
@@ -1489,7 +1475,7 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr * e_tag * mlty) =
| Tm_constant c ->
let _, ty, _ = TcTerm.typeof_tot_or_gtot_term (tcenv_of_uenv g) t true in //AR: TODO: type_of_well_typed?
let ml_ty = term_as_mlty g ty in
- with_ty ml_ty (mlexpr_of_const t.pos c), E_PURE, ml_ty
+ with_ty ml_ty (mlexpr_of_const' g t.pos c), E_PURE, ml_ty
| Tm_name _ -> //lookup in g; decide if its in left or right; tag is Pure because it's just a variable
if is_type g t //Here, we really need to be certain that g is a type; unclear if level ensures it
diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst
index 4bb77cae710..0b362ac1993 100644
--- a/src/parser/FStar.Parser.Const.fst
+++ b/src/parser/FStar.Parser.Const.fst
@@ -70,6 +70,7 @@ let int32_lid = p2l ["FStar"; "Int32"; "t"]
let uint32_lid = p2l ["FStar"; "UInt32"; "t"]
let int64_lid = p2l ["FStar"; "Int64"; "t"]
let uint64_lid = p2l ["FStar"; "UInt64"; "t"]
+let uint128_lid = p2l ["FStar"; "UInt128"; "t"]
let sizet_lid = p2l ["FStar"; "SizeT"; "t"]
let salloc_lid = p2l ["FStar"; "ST"; "salloc"]
@@ -402,7 +403,7 @@ let const_to_string x = match x with
| Const_bool b -> if b then "true" else "false"
| Const_real r -> r^"R"
| Const_string(s, _) -> U.format1 "\"%s\"" s
- | Const_int (x, _) -> x
+ | Const_int (x, _) -> x // FIXME
| Const_char c -> "'" ^ U.string_of_char c ^ "'"
| Const_range r -> FStar.Compiler.Range.string_of_range r
| Const_range_of -> "range_of"
diff --git a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst
index 1896f22bb1c..570603dae2d 100644
--- a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst
+++ b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst
@@ -356,7 +356,7 @@ let rec encode_const c env =
| Const_char c -> mkApp("FStar.Char.__char_of_int", [boxInt (mkInteger' (BU.int_of_char c))]), []
| Const_int (i, None) -> boxInt (mkInteger i), []
| Const_int (repr, Some sw) ->
- let syntax_term = FStar.ToSyntax.ToSyntax.desugar_machine_integer env.tcenv.dsenv repr sw Range.dummyRange in
+ let syntax_term = FStar.ToSyntax.ToSyntax.unfold_machine_integer env.tcenv.dsenv repr sw Range.dummyRange in
encode_term syntax_term env
| Const_string(s, _) -> Term.boxString <| mk_String_const s, []
| Const_range _ -> mk_Range_const (), []
@@ -367,8 +367,8 @@ let rec encode_const c env =
and encode_binders (fuel_opt:option term) (bs:Syntax.binders) (env:env_t) :
(list fv (* translated bound variables *)
* list term (* guards *)
- * env_t (* extended context *)
- * decls_t (* top-level decls to be emitted *)
+ * env_t (* extended context *)
+ * decls_t (* top-level decls to be emitted *)
* list bv) (* names *) =
if Env.debug env.tcenv Options.Medium then BU.print1 "Encoding binders %s\n" (Print.binders_to_string ", " bs);
diff --git a/src/smtencoding/FStar.SMTEncoding.Term.fst b/src/smtencoding/FStar.SMTEncoding.Term.fst
index c393c1e4b60..24a6689358d 100644
--- a/src/smtencoding/FStar.SMTEncoding.Term.fst
+++ b/src/smtencoding/FStar.SMTEncoding.Term.fst
@@ -52,7 +52,7 @@ F* would encode this to SMT as (roughly)
```
(declare-fun n () Term)
(assert (HasType n u32))
-(assert (n = U32.uint_to_to 0))
+(assert (n = U32.uint_to_t 0))
```
i.e., ground facts about the `n`'s typing and definition would be
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
index b0a2ebae20a..3b2b39c1025 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -1114,41 +1114,18 @@ and desugar_machine_integer env repr (signedness, width) range =
let tnm = if width = Sizet then "FStar.SizeT" else
"FStar." ^
(match signedness with | Unsigned -> "U" | Signed -> "") ^ "Int" ^
- (match width with | Int8 -> "8" | Int16 -> "16" | Int32 -> "32" | Int64 -> "64")
+ (match width with | Int8 -> "8" | Int16 -> "16" | Int32 -> "32" | Int64 -> "64" | Int128 -> "128")
in
- //we do a static check of integer constants
- //and coerce them to the appropriate type using the internal coercion
- // __uint_to_t or __int_to_t
- //Rather than relying on a verification condition to check this trivial property
+ // We do a static check of integer constants
+ // And simply create the relevant Tm_constant node
+ // Rather than relying on a verification condition to check this trivial property
if not (within_bounds repr signedness width)
then FStar.Errors.log_issue
range
(Errors.Error_OutOfRange,
BU.format2 "%s is not in the expected range for %s" repr tnm);
- let private_intro_nm = tnm ^
- ".__" ^ (match signedness with | Unsigned -> "u" | Signed -> "") ^ "int_to_t"
- in
- let intro_nm = tnm ^
- "." ^ (match signedness with | Unsigned -> "u" | Signed -> "") ^ "int_to_t"
- in
- let lid = lid_of_path (path_of_text intro_nm) range in
- let lid =
- match Env.try_lookup_lid env lid with
- | Some intro_term ->
- begin match intro_term.n with
- | Tm_fvar fv ->
- let private_lid = lid_of_path (path_of_text private_intro_nm) range in
- let private_fv = S.lid_and_dd_as_fv private_lid (U.incr_delta_depth (Some?.v fv.fv_delta)) fv.fv_qual in
- {intro_term with n=Tm_fvar private_fv}
- | _ ->
- failwith ("Unexpected non-fvar for " ^ intro_nm)
- end
- | None ->
- raise_error (Errors.Fatal_UnexpectedNumericLiteral, (BU.format1 "Unexpected numeric literal. Restart F* to load %s." tnm)) range in
- let repr' = S.mk (Tm_constant (Const_int (repr, None))) range in
- let app = S.mk (Tm_app {hd=lid; args=[repr', S.as_aqual_implicit false]}) range in
- S.mk (Tm_meta {tm=app;
- meta=Meta_desugared (Machine_integer (signedness, width))}) range
+ let c : FStar.Const.sconst = Const_int (repr, Some (signedness, width)) in
+ S.mk (Tm_constant c) range
and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term * antiquotations_temp =
let mk e = S.mk e top.range in
@@ -4398,3 +4375,25 @@ let add_modul_to_env_core (finish: bool) (m:Syntax.modul)
let add_partial_modul_to_env = add_modul_to_env_core false
let add_modul_to_env = add_modul_to_env_core true
+
+let unfold_machine_integer env repr (signedness, width) range =
+ let tnm = if width = Sizet then "FStar.SizeT" else
+ "FStar." ^
+ (match signedness with | Unsigned -> "U" | Signed -> "") ^ "Int" ^
+ (match width with | Int8 -> "8" | Int16 -> "16" | Int32 -> "32" | Int64 -> "64" | Int128 -> "128")
+ in
+ let intro_nm = tnm ^
+ "." ^ (match signedness with | Unsigned -> "u" | Signed -> "") ^ "int_to_t"
+ in
+ let lid = lid_of_path (path_of_text intro_nm) range in
+ let hd =
+ match Env.try_lookup_lid env lid with
+ | Some intro_term ->
+ intro_term
+ | None ->
+ raise_error (Errors.Fatal_UnexpectedNumericLiteral, (BU.format1 "Unexpected numeric literal. Restart F* to load %s." tnm)) range
+ in
+ let repr' = S.mk (Tm_constant (Const_int (repr, None))) range in
+ let app = S.mk (Tm_app {hd; args=[repr', S.as_aqual_implicit false]}) range in
+ S.mk (Tm_meta {tm=app;
+ meta=Meta_desugared (Machine_integer (signedness, width))}) range
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti b/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti
index 90351a67ddb..42ff808a78a 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fsti
@@ -32,9 +32,6 @@ module U = FStar.Syntax.Util
val as_interface: AST.modul -> AST.modul
val desugar_term: env -> term -> S.term
-val desugar_machine_integer: env -> repr:string
- -> (FStar.Const.signedness * FStar.Const.width)
- -> Range.range -> Syntax.term
val free_vars (tvars_only:bool) (e:env) (t:term) : list ident
val close: env -> term -> term
@@ -55,3 +52,7 @@ val parse_attr_with_list : bool -> S.term -> lident -> option (list int) * bool
val get_fail_attr1 : bool -> S.term -> option (list int * bool)
val get_fail_attr : bool -> list S.term -> option (list int * bool)
+
+val unfold_machine_integer: env -> repr:string
+ -> (FStar.Const.signedness * FStar.Const.width)
+ -> Range.range -> Syntax.term
diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst
index 30ab7dd5f54..14c410553f0 100644
--- a/src/typechecker/FStar.TypeChecker.Core.fst
+++ b/src/typechecker/FStar.TypeChecker.Core.fst
@@ -1600,7 +1600,7 @@ and check_pat (g:env) (p:pat) (t_sc:typ) : result (binders & universes) =
let e =
match c with
| FStar.Const.Const_int(repr, Some sw) ->
- FStar.ToSyntax.ToSyntax.desugar_machine_integer g.tcenv.dsenv repr sw p.p
+ FStar.ToSyntax.ToSyntax.unfold_machine_integer g.tcenv.dsenv repr sw p.p
| _ ->
mk (Tm_constant c) p.p in
let! _, t_const = check "pat_const" g e in
diff --git a/src/typechecker/FStar.TypeChecker.PatternUtils.fst b/src/typechecker/FStar.TypeChecker.PatternUtils.fst
index 92a96fcfcea..cb91a687f87 100644
--- a/src/typechecker/FStar.TypeChecker.PatternUtils.fst
+++ b/src/typechecker/FStar.TypeChecker.PatternUtils.fst
@@ -128,7 +128,7 @@ let raw_pat_as_exp (env:Env.env) (p:pat)
let e =
match c with
| FStar.Const.Const_int(repr, Some sw) ->
- FStar.ToSyntax.ToSyntax.desugar_machine_integer env.dsenv repr sw p.p
+ FStar.ToSyntax.ToSyntax.unfold_machine_integer env.dsenv repr sw p.p
| _ ->
mk (Tm_constant c) p.p
in
@@ -199,7 +199,7 @@ let pat_as_exp (introduce_bv_uvars:bool)
let e =
match c with
| FStar.Const.Const_int(repr, Some sw) ->
- FStar.ToSyntax.ToSyntax.desugar_machine_integer env.dsenv repr sw p.p
+ FStar.ToSyntax.ToSyntax.unfold_machine_integer env.dsenv repr sw p.p
| _ ->
mk (Tm_constant c) p.p
in
diff --git a/src/typechecker/FStar.TypeChecker.Primops.MachineInts.fst b/src/typechecker/FStar.TypeChecker.Primops.MachineInts.fst
index a434f594889..98dda4a7907 100644
--- a/src/typechecker/FStar.TypeChecker.Primops.MachineInts.fst
+++ b/src/typechecker/FStar.TypeChecker.Primops.MachineInts.fst
@@ -26,6 +26,9 @@ let bounded_arith_ops_for (k : machint_kind) : mymon unit =
(* Operators common to all *)
emit [
mk1 0 (nm "v") (v #k);
+ mk1 0 (nm (if is_unsigned k
+ then "uint_to_t"
+ else "int_to_t")) (int_to_t #k);
(* basic ops supported by all *)
mk2 0 (nm "add") (fun (x y : machint k) -> make_as x (Z.add_big_int (v x) (v y)));
@@ -39,7 +42,7 @@ let bounded_arith_ops_for (k : machint_kind) : mymon unit =
];!
(* Unsigned ints have more operators *)
- let sz = width k in
+ let sz = widthn k in
let modulus = Z.shift_left_big_int Z.one (Z.of_int_fs sz) in
let mod (x : Z.t) : Z.t = Z.mod_big_int x modulus in
if is_unsigned k then
@@ -90,5 +93,5 @@ let ops : list primitive_step =
emit [
(* Single extra op that returns a U32 *)
mk1 0 PC.char_u32_of_char (fun (c : char) -> let n = Compiler.Util.int_of_char c |> Z.of_int_fs in
- MachineInts.mk #UInt32 n None);
+ MachineInts.mk #UInt32 n);
])
diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst
index b2ec649f3f4..e78c9eeca26 100644
--- a/src/typechecker/FStar.TypeChecker.TcTerm.fst
+++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst
@@ -1864,6 +1864,7 @@ and tc_constant (env:env_t) r (c:sconst) : typ =
| Unsigned, Int16 -> Const.uint16_lid
| Unsigned, Int32 -> Const.uint32_lid
| Unsigned, Int64 -> Const.uint64_lid
+ | Unsigned, Int128 -> Const.uint128_lid
| Unsigned, Sizet -> Const.sizet_lid)
| Const_string _ -> t_string
| Const_real _ -> t_real
diff --git a/tests/bug-reports/Bug2699.ml.expected b/tests/bug-reports/Bug2699.ml.expected
index 8cfa2067184..f894e38a6d8 100644
--- a/tests/bug-reports/Bug2699.ml.expected
+++ b/tests/bug-reports/Bug2699.ml.expected
@@ -1,7 +1,5 @@
open Prims
let (broken_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)) =
- ((FStar_UInt32.uint_to_t (Prims.of_int (24))),
- (FStar_UInt32.uint_to_t (Prims.of_int (28))))
+ ((Stdint.Uint32.of_int (24)), (Stdint.Uint32.of_int (28)))
let (works_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)) =
- ((FStar_UInt32.uint_to_t (Prims.of_int (24))),
- (FStar_UInt32.uint_to_t (Prims.of_int (28))))
\ No newline at end of file
+ ((Stdint.Uint32.of_int (24)), (Stdint.Uint32.of_int (28)))
\ No newline at end of file
diff --git a/tests/ide/emacs/integration.push-pop.out.expected b/tests/ide/emacs/integration.push-pop.out.expected
index 0e073ecfc6b..888d3f7e668 100644
--- a/tests/ide/emacs/integration.push-pop.out.expected
+++ b/tests/ide/emacs/integration.push-pop.out.expected
@@ -98,7 +98,7 @@
{"kind": "response", "query-id": "164", "response": [], "status": "success"}
{"kind": "response", "query-id": "165", "response": [{"level": "error", "message": " - Assertion failed\n - The SMT solver could not prove the query. Use --query_stats for more\n details.\n - See also (13,15-13,23)\n", "number": 19, "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"}
{"kind": "response", "query-id": "170", "response": [], "status": "success"}
-{"kind": "response", "query-id": "175", "response": [{"level": "error", "message": " - Unexpected numeric literal. Restart F* to load FStar.UInt8.\n", "number": 201, "ranges": [{"beg": [13, 22], "end": [13, 24], "fname": ""}]}], "status": "success"}
+{"kind": "response", "query-id": "175", "response": [{"level": "error", "message": " - Expected expression of type int got expression 2uy of type FStar.UInt8.t\n", "number": 189, "ranges": [{"beg": [13, 22], "end": [13, 24], "fname": ""}]}], "status": "success"}
{"kind": "response", "query-id": "179", "response": [], "status": "success"}
{"kind": "response", "query-id": "180", "response": [{"level": "error", "message": " - Assertion failed\n - The SMT solver could not prove the query. Use --query_stats for more\n details.\n - See also (13,15-13,24)\n", "number": 19, "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 24], "fname": ""}]}], "status": "failure"}
{"kind": "response", "query-id": "185", "response": [], "status": "success"}
diff --git a/tests/machine_integers/Makefile b/tests/machine_integers/Makefile
index e408ed4ba87..474c8b416a9 100644
--- a/tests/machine_integers/Makefile
+++ b/tests/machine_integers/Makefile
@@ -15,6 +15,7 @@ accept: $(patsubst %.fst,%.run-accept,$(MODULES))
%.exe: %.fst | out
$(call msg, "BUILD", $(notdir $@))
$(eval B := $(patsubst %.exe,%,$@))
+ rm -f "out/${B}.ml"
$(Q)$(FSTAR) $(SIL) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml --extract '${B}' '${B}.fst'
$(Q)/bin/echo -e '\n\nlet _ = main ()\n' >> out/${B}.ml
$(Q)$(OCAMLOPT) out/${B}.ml -o $@
diff --git a/tests/machine_integers/TestMisc.fst b/tests/machine_integers/TestMisc.fst
new file mode 100644
index 00000000000..589fef1d38b
--- /dev/null
+++ b/tests/machine_integers/TestMisc.fst
@@ -0,0 +1,14 @@
+module TestMisc
+
+module U32 = FStar.UInt32
+
+#set-options "--no_smt"
+
+let _ = assert_norm (UInt.size 0 32)
+let _ = assert_norm (UInt.size 1 32)
+let _ = assert_norm (UInt.size 4294967295 32)
+
+[@@expect_failure]
+let _ = assert_norm (UInt.size 4294967296 32)
+
+let main () : FStar.All.ML unit = ()
diff --git a/tests/machine_integers/TestMisc.out.expected b/tests/machine_integers/TestMisc.out.expected
new file mode 100644
index 00000000000..e69de29bb2d