diff --git a/ocaml/fstar-lib/FStar_Range.ml b/ocaml/fstar-lib/FStar_Range.ml index 0451f197f82..e58e2d5aa94 100644 --- a/ocaml/fstar-lib/FStar_Range.ml +++ b/ocaml/fstar-lib/FStar_Range.ml @@ -5,4 +5,11 @@ let mk_range f a b c d = FStar_Compiler_Range_Type.mk_range f {line=a;col=b} {li let range_0 : range = let z = Prims.parse_int "0" in mk_range "dummy" z z z z let join_range r1 r2 = FStar_Compiler_Range_Ops.union_ranges r1 r2 +let explode (r:__range) = + (r.use_range.file_name, + r.use_range.start_pos.line, + r.use_range.start_pos.col, + r.use_range.end_pos.line, + r.use_range.end_pos.col) + type ('Ar,'Amsg,'Ab) labeled = 'Ab diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index f808795e646..10006c2add0 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -262,6 +262,10 @@ let (__range_lid : FStar_Ident.lident) = p2l ["FStar"; "Range"; "__range"] let (range_lid : FStar_Ident.lident) = p2l ["FStar"; "Range"; "range"] let (range_0 : FStar_Ident.lident) = p2l ["FStar"; "Range"; "range_0"] let (mk_range_lid : FStar_Ident.lident) = p2l ["FStar"; "Range"; "mk_range"] +let (__mk_range_lid : FStar_Ident.lident) = + p2l ["FStar"; "Range"; "__mk_range"] +let (__explode_range_lid : FStar_Ident.lident) = + p2l ["FStar"; "Range"; "explode"] let (join_range_lid : FStar_Ident.lident) = p2l ["FStar"; "Range"; "join_range"] let (guard_free : FStar_Ident.lident) = pconst "guard_free" @@ -409,6 +413,10 @@ let (lid_tuple2 : FStar_Ident.lident) = mk_tuple_lid (Prims.of_int (2)) FStar_Compiler_Range_Type.dummyRange let (lid_tuple3 : FStar_Ident.lident) = mk_tuple_lid (Prims.of_int (3)) FStar_Compiler_Range_Type.dummyRange +let (lid_tuple4 : FStar_Ident.lident) = + mk_tuple_lid (Prims.of_int (4)) FStar_Compiler_Range_Type.dummyRange +let (lid_tuple5 : FStar_Ident.lident) = + mk_tuple_lid (Prims.of_int (5)) FStar_Compiler_Range_Type.dummyRange let (is_tuple_constructor_string : Prims.string -> Prims.bool) = fun s -> FStar_Compiler_Util.starts_with s "FStar.Pervasives.Native.tuple" let (is_tuple_constructor_id : FStar_Ident.ident -> Prims.bool) = @@ -431,6 +439,10 @@ let (lid_Mktuple2 : FStar_Ident.lident) = mk_tuple_data_lid (Prims.of_int (2)) FStar_Compiler_Range_Type.dummyRange let (lid_Mktuple3 : FStar_Ident.lident) = mk_tuple_data_lid (Prims.of_int (3)) FStar_Compiler_Range_Type.dummyRange +let (lid_Mktuple4 : FStar_Ident.lident) = + mk_tuple_data_lid (Prims.of_int (4)) FStar_Compiler_Range_Type.dummyRange +let (lid_Mktuple5 : FStar_Ident.lident) = + mk_tuple_data_lid (Prims.of_int (5)) FStar_Compiler_Range_Type.dummyRange let (is_tuple_datacon_string : Prims.string -> Prims.bool) = fun s -> FStar_Compiler_Util.starts_with s "FStar.Pervasives.Native.Mktuple" diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml index 34bd42f3e05..78bc5c739b6 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml @@ -505,7 +505,7 @@ let e_tuple2 : let uu___1 = FStar_Syntax_Embeddings_Base.type_of ea in let uu___2 = FStar_Syntax_Embeddings_Base.type_of eb in FStar_Syntax_Syntax.t_tuple2_of uu___1 uu___2 in - let emb_t_pair_a_b uu___ = + let emb_t_pair uu___ = let uu___1 = let uu___2 = FStar_Ident.string_of_lid FStar_Parser_Const.lid_tuple2 in @@ -528,7 +528,7 @@ let e_tuple2 : uu___3 y in FStar_Compiler_Util.format2 "(%s, %s)" uu___1 uu___2 in let em x rng shadow norm = - lazy_embed printer1 emb_t_pair_a_b rng typ x + lazy_embed printer1 emb_t_pair rng typ x (fun uu___ -> let proj i ab = let proj_1 = @@ -597,34 +597,52 @@ let e_tuple2 : uu___3 :: uu___4 in FStar_Syntax_Syntax.mk_Tm_app uu___1 uu___2 rng) in let un t norm = - lazy_unembed printer1 emb_t_pair_a_b t typ - (fun t1 -> - let uu___ = FStar_Syntax_Util.head_and_args_full t1 in - match uu___ with - | (hd, args) -> - let uu___1 = - let uu___2 = - let uu___3 = FStar_Syntax_Util.un_uinst hd in - uu___3.FStar_Syntax_Syntax.n in - (uu___2, args) in - (match uu___1 with - | (FStar_Syntax_Syntax.Tm_fvar fv, - uu___2::uu___3::(a1, uu___4)::(b1, uu___5)::[]) when - FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.lid_Mktuple2 - -> - let uu___6 = - FStar_Syntax_Embeddings_Base.try_unembed ea a1 norm in - FStar_Compiler_Util.bind_opt uu___6 - (fun a2 -> - let uu___7 = - FStar_Syntax_Embeddings_Base.try_unembed eb b1 - norm in - FStar_Compiler_Util.bind_opt uu___7 - (fun b2 -> FStar_Pervasives_Native.Some (a2, b2))) - | uu___2 -> FStar_Pervasives_Native.None)) in - FStar_Syntax_Embeddings_Base.mk_emb_full em un typ printer1 - emb_t_pair_a_b + lazy_unembed printer1 emb_t_pair t typ + (fun uu___ -> + (fun t1 -> + let uu___ = FStar_Syntax_Util.head_and_args_full t1 in + match uu___ with + | (hd, args) -> + let uu___1 = + let uu___2 = + let uu___3 = FStar_Syntax_Util.un_uinst hd in + uu___3.FStar_Syntax_Syntax.n in + (uu___2, args) in + (match uu___1 with + | (FStar_Syntax_Syntax.Tm_fvar fv, + uu___2::uu___3::(a1, uu___4)::(b1, uu___5)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.lid_Mktuple2 + -> + Obj.magic + (Obj.repr + (let uu___6 = + FStar_Syntax_Embeddings_Base.try_unembed ea + a1 norm in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___6) + (fun uu___7 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___7 = + FStar_Syntax_Embeddings_Base.try_unembed + eb b1 norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () + () (Obj.magic uu___7) + (fun uu___8 -> + (fun b2 -> + let b2 = Obj.magic b2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2))) uu___8))) + uu___7))) + | uu___2 -> + Obj.magic (Obj.repr FStar_Pervasives_Native.None))) + uu___) in + FStar_Syntax_Embeddings_Base.mk_emb_full em un typ printer1 emb_t_pair let e_tuple3 : 'a 'b 'c . 'a FStar_Syntax_Embeddings_Base.embedding -> @@ -640,7 +658,7 @@ let e_tuple3 : let uu___2 = FStar_Syntax_Embeddings_Base.type_of eb in let uu___3 = FStar_Syntax_Embeddings_Base.type_of ec in FStar_Syntax_Syntax.t_tuple3_of uu___1 uu___2 uu___3 in - let emb_t_pair_a_b_c uu___ = + let emb_t_pair uu___ = let uu___1 = let uu___2 = FStar_Ident.string_of_lid FStar_Parser_Const.lid_tuple3 in @@ -671,7 +689,7 @@ let e_tuple3 : let em uu___ rng shadow norm = match uu___ with | (x1, x2, x3) -> - lazy_embed printer1 emb_t_pair_a_b_c rng typ (x1, x2, x3) + lazy_embed printer1 emb_t_pair rng typ (x1, x2, x3) (fun uu___1 -> let proj i abc = let proj_i = @@ -764,42 +782,666 @@ let e_tuple3 : uu___4 :: uu___5 in FStar_Syntax_Syntax.mk_Tm_app uu___2 uu___3 rng) in let un t norm = - lazy_unembed printer1 emb_t_pair_a_b_c t typ - (fun t1 -> - let uu___ = FStar_Syntax_Util.head_and_args_full t1 in - match uu___ with - | (hd, args) -> - let uu___1 = + lazy_unembed printer1 emb_t_pair t typ + (fun uu___ -> + (fun t1 -> + let uu___ = FStar_Syntax_Util.head_and_args_full t1 in + match uu___ with + | (hd, args) -> + let uu___1 = + let uu___2 = + let uu___3 = FStar_Syntax_Util.un_uinst hd in + uu___3.FStar_Syntax_Syntax.n in + (uu___2, args) in + (match uu___1 with + | (FStar_Syntax_Syntax.Tm_fvar fv, + uu___2::uu___3::uu___4::(a1, uu___5)::(b1, uu___6):: + (c1, uu___7)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.lid_Mktuple3 + -> + Obj.magic + (Obj.repr + (let uu___8 = + FStar_Syntax_Embeddings_Base.try_unembed + ea a1 norm in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___8) + (fun uu___9 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___9 = + FStar_Syntax_Embeddings_Base.try_unembed + eb b1 norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () (Obj.magic uu___9) + (fun uu___10 -> + (fun b2 -> + let b2 = Obj.magic b2 in + let uu___10 = + FStar_Syntax_Embeddings_Base.try_unembed + ec c1 norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___10) + (fun uu___11 -> + (fun c2 -> + let c2 = + Obj.magic c2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2, + c2))) + uu___11))) + uu___10))) uu___9))) + | uu___2 -> + Obj.magic (Obj.repr FStar_Pervasives_Native.None))) + uu___) in + FStar_Syntax_Embeddings_Base.mk_emb_full em un typ printer1 + emb_t_pair +let e_tuple4 : + 'a 'b 'c 'd . + 'a FStar_Syntax_Embeddings_Base.embedding -> + 'b FStar_Syntax_Embeddings_Base.embedding -> + 'c FStar_Syntax_Embeddings_Base.embedding -> + 'd FStar_Syntax_Embeddings_Base.embedding -> + ('a * 'b * 'c * 'd) FStar_Syntax_Embeddings_Base.embedding + = + fun ea -> + fun eb -> + fun ec -> + fun ed -> + let typ uu___ = + let uu___1 = FStar_Syntax_Embeddings_Base.type_of ea in + let uu___2 = FStar_Syntax_Embeddings_Base.type_of eb in + let uu___3 = FStar_Syntax_Embeddings_Base.type_of ec in + let uu___4 = FStar_Syntax_Embeddings_Base.type_of ed in + FStar_Syntax_Syntax.t_tuple4_of uu___1 uu___2 uu___3 uu___4 in + let emb_t_pair uu___ = + let uu___1 = + let uu___2 = + FStar_Ident.string_of_lid FStar_Parser_Const.lid_tuple4 in + let uu___3 = + let uu___4 = FStar_Syntax_Embeddings_Base.emb_typ_of ea () in + let uu___5 = + let uu___6 = FStar_Syntax_Embeddings_Base.emb_typ_of eb () in + let uu___7 = + let uu___8 = + FStar_Syntax_Embeddings_Base.emb_typ_of ec () in + let uu___9 = + let uu___10 = + FStar_Syntax_Embeddings_Base.emb_typ_of ed () in + [uu___10] in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + (uu___2, uu___3) in + FStar_Syntax_Syntax.ET_app uu___1 in + let printer1 uu___ = + match uu___ with + | (x, y, z, w) -> + let uu___1 = + let uu___2 = FStar_Syntax_Embeddings_Base.printer_of ea in + uu___2 x in + let uu___2 = + let uu___3 = FStar_Syntax_Embeddings_Base.printer_of eb in + uu___3 y in + let uu___3 = + let uu___4 = FStar_Syntax_Embeddings_Base.printer_of ec in + uu___4 z in + let uu___4 = + let uu___5 = FStar_Syntax_Embeddings_Base.printer_of ed in + uu___5 w in + FStar_Compiler_Util.format4 "(%s, %s, %s, %s)" uu___1 uu___2 + uu___3 uu___4 in + let em uu___ rng shadow norm = + match uu___ with + | (x1, x2, x3, x4) -> + lazy_embed printer1 emb_t_pair rng typ (x1, x2, x3, x4) + (fun uu___1 -> + let proj i abcd = + let proj_i = + let uu___2 = + FStar_Parser_Const.mk_tuple_data_lid + (Prims.of_int (4)) rng in + let uu___3 = + FStar_Syntax_Syntax.null_bv + FStar_Syntax_Syntax.tun in + FStar_Syntax_Util.mk_field_projector_name uu___2 + uu___3 i in + let proj_i_tm = + let uu___2 = + FStar_Syntax_Syntax.lid_as_fv proj_i + FStar_Pervasives_Native.None in + FStar_Syntax_Syntax.fv_to_tm uu___2 in + let uu___2 = + FStar_Syntax_Syntax.mk_Tm_uinst proj_i_tm + [FStar_Syntax_Syntax.U_zero] in + let uu___3 = + let uu___4 = + let uu___5 = + FStar_Syntax_Embeddings_Base.type_of ea in + FStar_Syntax_Syntax.iarg uu___5 in + let uu___5 = + let uu___6 = + let uu___7 = + FStar_Syntax_Embeddings_Base.type_of eb in + FStar_Syntax_Syntax.iarg uu___7 in + let uu___7 = + let uu___8 = + let uu___9 = + FStar_Syntax_Embeddings_Base.type_of ec in + FStar_Syntax_Syntax.iarg uu___9 in + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Syntax_Embeddings_Base.type_of ed in + FStar_Syntax_Syntax.iarg uu___11 in + let uu___11 = + let uu___12 = + FStar_Syntax_Syntax.as_arg abcd in + [uu___12] in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + FStar_Syntax_Syntax.mk_Tm_app uu___2 uu___3 rng in + let shadow_a = map_shadow shadow (proj Prims.int_one) in + let shadow_b = + map_shadow shadow (proj (Prims.of_int (2))) in + let shadow_c = + map_shadow shadow (proj (Prims.of_int (3))) in + let shadow_d = + map_shadow shadow (proj (Prims.of_int (4))) in let uu___2 = - let uu___3 = FStar_Syntax_Util.un_uinst hd in - uu___3.FStar_Syntax_Syntax.n in - (uu___2, args) in - (match uu___1 with - | (FStar_Syntax_Syntax.Tm_fvar fv, - uu___2::uu___3::uu___4::(a1, uu___5)::(b1, uu___6):: - (c1, uu___7)::[]) when - FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.lid_Mktuple3 - -> - let uu___8 = - FStar_Syntax_Embeddings_Base.try_unembed ea a1 norm in - FStar_Compiler_Util.bind_opt uu___8 - (fun a2 -> + let uu___3 = + FStar_Syntax_Syntax.tdataconstr + FStar_Parser_Const.lid_Mktuple4 in + FStar_Syntax_Syntax.mk_Tm_uinst uu___3 + [FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero] in + let uu___3 = + let uu___4 = + let uu___5 = FStar_Syntax_Embeddings_Base.type_of ea in + FStar_Syntax_Syntax.iarg uu___5 in + let uu___5 = + let uu___6 = + let uu___7 = + FStar_Syntax_Embeddings_Base.type_of eb in + FStar_Syntax_Syntax.iarg uu___7 in + let uu___7 = + let uu___8 = let uu___9 = - FStar_Syntax_Embeddings_Base.try_unembed eb b1 - norm in - FStar_Compiler_Util.bind_opt uu___9 - (fun b2 -> - let uu___10 = - FStar_Syntax_Embeddings_Base.try_unembed - ec c1 norm in - FStar_Compiler_Util.bind_opt uu___10 - (fun c2 -> - FStar_Pervasives_Native.Some - (a2, b2, c2)))) - | uu___2 -> FStar_Pervasives_Native.None)) in - FStar_Syntax_Embeddings_Base.mk_emb_full em un typ printer1 - emb_t_pair_a_b_c + FStar_Syntax_Embeddings_Base.type_of ec in + FStar_Syntax_Syntax.iarg uu___9 in + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Syntax_Embeddings_Base.type_of ed in + FStar_Syntax_Syntax.iarg uu___11 in + let uu___11 = + let uu___12 = + let uu___13 = + let uu___14 = + FStar_Syntax_Embeddings_Base.embed ea x1 in + uu___14 rng shadow_a norm in + FStar_Syntax_Syntax.as_arg uu___13 in + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = + FStar_Syntax_Embeddings_Base.embed eb + x2 in + uu___16 rng shadow_b norm in + FStar_Syntax_Syntax.as_arg uu___15 in + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 = + FStar_Syntax_Embeddings_Base.embed + ec x3 in + uu___18 rng shadow_c norm in + FStar_Syntax_Syntax.as_arg uu___17 in + let uu___17 = + let uu___18 = + let uu___19 = + let uu___20 = + FStar_Syntax_Embeddings_Base.embed + ed x4 in + uu___20 rng shadow_d norm in + FStar_Syntax_Syntax.as_arg uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + FStar_Syntax_Syntax.mk_Tm_app uu___2 uu___3 rng) in + let un t norm = + lazy_unembed printer1 emb_t_pair t typ + (fun uu___ -> + (fun t1 -> + let uu___ = FStar_Syntax_Util.head_and_args_full t1 in + match uu___ with + | (hd, args) -> + let uu___1 = + let uu___2 = + let uu___3 = FStar_Syntax_Util.un_uinst hd in + uu___3.FStar_Syntax_Syntax.n in + (uu___2, args) in + (match uu___1 with + | (FStar_Syntax_Syntax.Tm_fvar fv, + uu___2::uu___3::uu___4::uu___5::(a1, uu___6):: + (b1, uu___7)::(c1, uu___8)::(d1, uu___9)::[]) + when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.lid_Mktuple4 + -> + Obj.magic + (Obj.repr + (let uu___10 = + FStar_Syntax_Embeddings_Base.try_unembed + ea a1 norm in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___10) + (fun uu___11 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___11 = + FStar_Syntax_Embeddings_Base.try_unembed + eb b1 norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () (Obj.magic uu___11) + (fun uu___12 -> + (fun b2 -> + let b2 = Obj.magic b2 in + let uu___12 = + FStar_Syntax_Embeddings_Base.try_unembed + ec c1 norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___12) + (fun uu___13 -> + (fun c2 -> + let c2 = + Obj.magic + c2 in + let uu___13 + = + FStar_Syntax_Embeddings_Base.try_unembed + ed d1 + norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___13) + (fun + uu___14 + -> + (fun d2 + -> + let d2 = + Obj.magic + d2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2, + c2, d2))) + uu___14))) + uu___13))) + uu___12))) uu___11))) + | uu___2 -> + Obj.magic + (Obj.repr FStar_Pervasives_Native.None))) + uu___) in + FStar_Syntax_Embeddings_Base.mk_emb_full em un typ printer1 + emb_t_pair +let e_tuple5 : + 'a 'b 'c 'd 'e . + 'a FStar_Syntax_Embeddings_Base.embedding -> + 'b FStar_Syntax_Embeddings_Base.embedding -> + 'c FStar_Syntax_Embeddings_Base.embedding -> + 'd FStar_Syntax_Embeddings_Base.embedding -> + 'e FStar_Syntax_Embeddings_Base.embedding -> + ('a * 'b * 'c * 'd * 'e) FStar_Syntax_Embeddings_Base.embedding + = + fun ea -> + fun eb -> + fun ec -> + fun ed -> + fun ee -> + let typ uu___ = + let uu___1 = FStar_Syntax_Embeddings_Base.type_of ea in + let uu___2 = FStar_Syntax_Embeddings_Base.type_of eb in + let uu___3 = FStar_Syntax_Embeddings_Base.type_of ec in + let uu___4 = FStar_Syntax_Embeddings_Base.type_of ed in + let uu___5 = FStar_Syntax_Embeddings_Base.type_of ee in + FStar_Syntax_Syntax.t_tuple5_of uu___1 uu___2 uu___3 uu___4 + uu___5 in + let emb_t_pair uu___ = + let uu___1 = + let uu___2 = + FStar_Ident.string_of_lid FStar_Parser_Const.lid_tuple5 in + let uu___3 = + let uu___4 = FStar_Syntax_Embeddings_Base.emb_typ_of ea () in + let uu___5 = + let uu___6 = + FStar_Syntax_Embeddings_Base.emb_typ_of eb () in + let uu___7 = + let uu___8 = + FStar_Syntax_Embeddings_Base.emb_typ_of ec () in + let uu___9 = + let uu___10 = + FStar_Syntax_Embeddings_Base.emb_typ_of ed () in + let uu___11 = + let uu___12 = + FStar_Syntax_Embeddings_Base.emb_typ_of ee () in + [uu___12] in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + (uu___2, uu___3) in + FStar_Syntax_Syntax.ET_app uu___1 in + let printer1 uu___ = + match uu___ with + | (x, y, z, w, v) -> + let uu___1 = + let uu___2 = FStar_Syntax_Embeddings_Base.printer_of ea in + uu___2 x in + let uu___2 = + let uu___3 = FStar_Syntax_Embeddings_Base.printer_of eb in + uu___3 y in + let uu___3 = + let uu___4 = FStar_Syntax_Embeddings_Base.printer_of ec in + uu___4 z in + let uu___4 = + let uu___5 = FStar_Syntax_Embeddings_Base.printer_of ed in + uu___5 w in + let uu___5 = + let uu___6 = FStar_Syntax_Embeddings_Base.printer_of ee in + uu___6 v in + FStar_Compiler_Util.format5 "(%s, %s, %s, %s, %s)" uu___1 + uu___2 uu___3 uu___4 uu___5 in + let em uu___ rng shadow norm = + match uu___ with + | (x1, x2, x3, x4, x5) -> + lazy_embed printer1 emb_t_pair rng typ (x1, x2, x3, x4, x5) + (fun uu___1 -> + let proj i abcde = + let proj_i = + let uu___2 = + FStar_Parser_Const.mk_tuple_data_lid + (Prims.of_int (5)) rng in + let uu___3 = + FStar_Syntax_Syntax.null_bv + FStar_Syntax_Syntax.tun in + FStar_Syntax_Util.mk_field_projector_name uu___2 + uu___3 i in + let proj_i_tm = + let uu___2 = + FStar_Syntax_Syntax.lid_as_fv proj_i + FStar_Pervasives_Native.None in + FStar_Syntax_Syntax.fv_to_tm uu___2 in + let uu___2 = + FStar_Syntax_Syntax.mk_Tm_uinst proj_i_tm + [FStar_Syntax_Syntax.U_zero] in + let uu___3 = + let uu___4 = + let uu___5 = + FStar_Syntax_Embeddings_Base.type_of ea in + FStar_Syntax_Syntax.iarg uu___5 in + let uu___5 = + let uu___6 = + let uu___7 = + FStar_Syntax_Embeddings_Base.type_of eb in + FStar_Syntax_Syntax.iarg uu___7 in + let uu___7 = + let uu___8 = + let uu___9 = + FStar_Syntax_Embeddings_Base.type_of ec in + FStar_Syntax_Syntax.iarg uu___9 in + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Syntax_Embeddings_Base.type_of ed in + FStar_Syntax_Syntax.iarg uu___11 in + let uu___11 = + let uu___12 = + let uu___13 = + FStar_Syntax_Embeddings_Base.type_of + ee in + FStar_Syntax_Syntax.iarg uu___13 in + let uu___13 = + let uu___14 = + FStar_Syntax_Syntax.as_arg abcde in + [uu___14] in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + FStar_Syntax_Syntax.mk_Tm_app uu___2 uu___3 rng in + let shadow_a = map_shadow shadow (proj Prims.int_one) in + let shadow_b = + map_shadow shadow (proj (Prims.of_int (2))) in + let shadow_c = + map_shadow shadow (proj (Prims.of_int (3))) in + let shadow_d = + map_shadow shadow (proj (Prims.of_int (4))) in + let shadow_e = + map_shadow shadow (proj (Prims.of_int (5))) in + let uu___2 = + let uu___3 = + FStar_Syntax_Syntax.tdataconstr + FStar_Parser_Const.lid_Mktuple5 in + FStar_Syntax_Syntax.mk_Tm_uinst uu___3 + [FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero] in + let uu___3 = + let uu___4 = + let uu___5 = + FStar_Syntax_Embeddings_Base.type_of ea in + FStar_Syntax_Syntax.iarg uu___5 in + let uu___5 = + let uu___6 = + let uu___7 = + FStar_Syntax_Embeddings_Base.type_of eb in + FStar_Syntax_Syntax.iarg uu___7 in + let uu___7 = + let uu___8 = + let uu___9 = + FStar_Syntax_Embeddings_Base.type_of ec in + FStar_Syntax_Syntax.iarg uu___9 in + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Syntax_Embeddings_Base.type_of ed in + FStar_Syntax_Syntax.iarg uu___11 in + let uu___11 = + let uu___12 = + let uu___13 = + FStar_Syntax_Embeddings_Base.type_of ee in + FStar_Syntax_Syntax.iarg uu___13 in + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = + FStar_Syntax_Embeddings_Base.embed + ea x1 in + uu___16 rng shadow_a norm in + FStar_Syntax_Syntax.as_arg uu___15 in + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 = + FStar_Syntax_Embeddings_Base.embed + eb x2 in + uu___18 rng shadow_b norm in + FStar_Syntax_Syntax.as_arg uu___17 in + let uu___17 = + let uu___18 = + let uu___19 = + let uu___20 = + FStar_Syntax_Embeddings_Base.embed + ec x3 in + uu___20 rng shadow_c norm in + FStar_Syntax_Syntax.as_arg uu___19 in + let uu___19 = + let uu___20 = + let uu___21 = + let uu___22 = + FStar_Syntax_Embeddings_Base.embed + ed x4 in + uu___22 rng shadow_d norm in + FStar_Syntax_Syntax.as_arg uu___21 in + let uu___21 = + let uu___22 = + let uu___23 = + let uu___24 = + FStar_Syntax_Embeddings_Base.embed + ee x5 in + uu___24 rng shadow_e norm in + FStar_Syntax_Syntax.as_arg + uu___23 in + [uu___22] in + uu___20 :: uu___21 in + uu___18 :: uu___19 in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + FStar_Syntax_Syntax.mk_Tm_app uu___2 uu___3 rng) in + let un t norm = + lazy_unembed printer1 emb_t_pair t typ + (fun uu___ -> + (fun t1 -> + let uu___ = FStar_Syntax_Util.head_and_args_full t1 in + match uu___ with + | (hd, args) -> + let uu___1 = + let uu___2 = + let uu___3 = FStar_Syntax_Util.un_uinst hd in + uu___3.FStar_Syntax_Syntax.n in + (uu___2, args) in + (match uu___1 with + | (FStar_Syntax_Syntax.Tm_fvar fv, + uu___2::uu___3::uu___4::uu___5::uu___6:: + (a1, uu___7)::(b1, uu___8)::(c1, uu___9):: + (d1, uu___10)::(e1, uu___11)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.lid_Mktuple5 + -> + Obj.magic + (Obj.repr + (let uu___12 = + FStar_Syntax_Embeddings_Base.try_unembed + ea a1 norm in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___12) + (fun uu___13 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___13 = + FStar_Syntax_Embeddings_Base.try_unembed + eb b1 norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () (Obj.magic uu___13) + (fun uu___14 -> + (fun b2 -> + let b2 = Obj.magic b2 in + let uu___14 = + FStar_Syntax_Embeddings_Base.try_unembed + ec c1 norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___14) + (fun uu___15 -> + (fun c2 -> + let c2 = + Obj.magic + c2 in + let uu___15 + = + FStar_Syntax_Embeddings_Base.try_unembed + ed d1 + norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___15) + (fun + uu___16 + -> + (fun d2 + -> + let d2 = + Obj.magic + d2 in + let uu___16 + = + FStar_Syntax_Embeddings_Base.try_unembed + ee e1 + norm in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___16) + (fun + uu___17 + -> + (fun e2 + -> + let e2 = + Obj.magic + e2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2, + c2, d2, + e2))) + uu___17))) + uu___16))) + uu___15))) + uu___14))) uu___13))) + | uu___2 -> + Obj.magic + (Obj.repr FStar_Pervasives_Native.None))) + uu___) in + FStar_Syntax_Embeddings_Base.mk_emb_full em un typ printer1 + emb_t_pair let e_either : 'a 'b . 'a FStar_Syntax_Embeddings_Base.embedding -> diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml index 1d0cabf8f76..b12991697f4 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml @@ -2983,6 +2983,48 @@ let (t_tuple3_of : term -> term -> term -> term) = uu___5 in uu___2 :: uu___3 in mk_Tm_app uu___ uu___1 FStar_Compiler_Range_Type.dummyRange +let (t_tuple4_of : term -> term -> term -> term -> term) = + fun t1 -> + fun t2 -> + fun t3 -> + fun t4 -> + let uu___ = + let uu___1 = tabbrev FStar_Parser_Const.lid_tuple4 in + mk_Tm_uinst uu___1 [U_zero; U_zero; U_zero; U_zero] in + let uu___1 = + let uu___2 = as_arg t1 in + let uu___3 = + let uu___4 = as_arg t2 in + let uu___5 = + let uu___6 = as_arg t3 in + let uu___7 = let uu___8 = as_arg t4 in [uu___8] in uu___6 :: + uu___7 in + uu___4 :: uu___5 in + uu___2 :: uu___3 in + mk_Tm_app uu___ uu___1 FStar_Compiler_Range_Type.dummyRange +let (t_tuple5_of : term -> term -> term -> term -> term -> term) = + fun t1 -> + fun t2 -> + fun t3 -> + fun t4 -> + fun t5 -> + let uu___ = + let uu___1 = tabbrev FStar_Parser_Const.lid_tuple5 in + mk_Tm_uinst uu___1 [U_zero; U_zero; U_zero; U_zero; U_zero] in + let uu___1 = + let uu___2 = as_arg t1 in + let uu___3 = + let uu___4 = as_arg t2 in + let uu___5 = + let uu___6 = as_arg t3 in + let uu___7 = + let uu___8 = as_arg t4 in + let uu___9 = let uu___10 = as_arg t5 in [uu___10] in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + uu___2 :: uu___3 in + mk_Tm_app uu___ uu___1 FStar_Compiler_Range_Type.dummyRange let (t_either_of : term -> term -> term) = fun t1 -> fun t2 -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml index 20536f14387..1df48fa2d9e 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml @@ -1716,12 +1716,16 @@ and (iapp : | FStar_TypeChecker_NBETerm.Constant (FStar_TypeChecker_NBETerm.SConst (FStar_Const.Const_range_of)) -> + let callbacks = + { + FStar_TypeChecker_NBETerm.iapp = (iapp cfg); + FStar_TypeChecker_NBETerm.translate = (translate cfg []) + } in (match args with | (a, uu___1)::[] -> - mk_rt a.FStar_TypeChecker_NBETerm.nbe_r - (FStar_TypeChecker_NBETerm.Constant - (FStar_TypeChecker_NBETerm.Range - (a.FStar_TypeChecker_NBETerm.nbe_r))) + FStar_TypeChecker_NBETerm.embed + FStar_TypeChecker_NBETerm.e_range callbacks + a.FStar_TypeChecker_NBETerm.nbe_r | uu___1 -> let uu___2 = let uu___3 = FStar_TypeChecker_NBETerm.t_to_string f in @@ -1731,19 +1735,24 @@ and (iapp : | FStar_TypeChecker_NBETerm.Constant (FStar_TypeChecker_NBETerm.SConst (FStar_Const.Const_set_range_of)) -> + let callbacks = + { + FStar_TypeChecker_NBETerm.iapp = (iapp cfg); + FStar_TypeChecker_NBETerm.translate = (translate cfg []) + } in (match args with - | (t, uu___1)::({ - FStar_TypeChecker_NBETerm.nbe_t = - FStar_TypeChecker_NBETerm.Constant - (FStar_TypeChecker_NBETerm.Range r); - FStar_TypeChecker_NBETerm.nbe_r = uu___2;_}, - uu___3)::[] - -> - { - FStar_TypeChecker_NBETerm.nbe_t = - (t.FStar_TypeChecker_NBETerm.nbe_t); - FStar_TypeChecker_NBETerm.nbe_r = r - } + | (t, uu___1)::(r, uu___2)::[] -> + let uu___3 = + FStar_TypeChecker_NBETerm.unembed + FStar_TypeChecker_NBETerm.e_range callbacks r in + (match uu___3 with + | FStar_Pervasives_Native.Some rr -> + { + FStar_TypeChecker_NBETerm.nbe_t = + (t.FStar_TypeChecker_NBETerm.nbe_t); + FStar_TypeChecker_NBETerm.nbe_r = rr + } + | FStar_Pervasives_Native.None -> Prims.magic ()) | uu___1 -> let uu___2 = let uu___3 = FStar_TypeChecker_NBETerm.t_to_string f in @@ -2804,7 +2813,7 @@ and (readback : | FStar_TypeChecker_NBETerm.Constant (FStar_TypeChecker_NBETerm.Range r) -> FStar_TypeChecker_Primops_Base.embed_simple - FStar_Syntax_Embeddings.e_range + FStar_Syntax_Embeddings.e___range x.FStar_TypeChecker_NBETerm.nbe_r r | FStar_TypeChecker_NBETerm.Constant (FStar_TypeChecker_NBETerm.Real r) -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml index 87023d1e7c4..a214e697f5d 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml @@ -1169,21 +1169,37 @@ let e_tuple2 : 'a 'b . 'a embedding -> 'b embedding -> ('a * 'b) embedding = uu___1) in let un1 cb trm = lazy_unembed etyp trm - (fun trm1 -> - match trm1.nbe_t with - | Construct - (fvar, us, (b1, uu___)::(a1, uu___1)::uu___2::uu___3::[]) - when - FStar_Syntax_Syntax.fv_eq_lid fvar - FStar_Parser_Const.lid_Mktuple2 - -> - let uu___4 = unembed ea cb a1 in - FStar_Compiler_Util.bind_opt uu___4 - (fun a2 -> - let uu___5 = unembed eb cb b1 in - FStar_Compiler_Util.bind_opt uu___5 - (fun b2 -> FStar_Pervasives_Native.Some (a2, b2))) - | uu___ -> FStar_Pervasives_Native.None) in + (fun uu___ -> + (fun trm1 -> + match trm1.nbe_t with + | Construct + (fvar, us, (b1, uu___)::(a1, uu___1)::uu___2::uu___3::[]) + when + FStar_Syntax_Syntax.fv_eq_lid fvar + FStar_Parser_Const.lid_Mktuple2 + -> + Obj.magic + (Obj.repr + (let uu___4 = unembed ea cb a1 in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___4) + (fun uu___5 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___5 = unembed eb cb b1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___5) + (fun uu___6 -> + (fun b2 -> + let b2 = Obj.magic b2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2))) uu___6))) uu___5))) + | uu___ -> Obj.magic (Obj.repr FStar_Pervasives_Native.None)) + uu___) in mk_emb em1 un1 (fun uu___ -> let uu___1 = @@ -1250,26 +1266,50 @@ let e_tuple3 : FStar_Syntax_Syntax.U_zero] uu___2) in let un1 cb trm = lazy_unembed etyp trm - (fun trm1 -> - match trm1.nbe_t with - | Construct - (fvar, us, - (c1, uu___)::(b1, uu___1)::(a1, uu___2)::uu___3::uu___4::[]) - when - FStar_Syntax_Syntax.fv_eq_lid fvar - FStar_Parser_Const.lid_Mktuple3 - -> - let uu___5 = unembed ea cb a1 in - FStar_Compiler_Util.bind_opt uu___5 - (fun a2 -> - let uu___6 = unembed eb cb b1 in - FStar_Compiler_Util.bind_opt uu___6 - (fun b2 -> - let uu___7 = unembed ec cb c1 in - FStar_Compiler_Util.bind_opt uu___7 - (fun c2 -> - FStar_Pervasives_Native.Some (a2, b2, c2)))) - | uu___ -> FStar_Pervasives_Native.None) in + (fun uu___ -> + (fun trm1 -> + match trm1.nbe_t with + | Construct + (fvar, us, + (c1, uu___)::(b1, uu___1)::(a1, uu___2)::uu___3::uu___4::uu___5::[]) + when + FStar_Syntax_Syntax.fv_eq_lid fvar + FStar_Parser_Const.lid_Mktuple3 + -> + Obj.magic + (Obj.repr + (let uu___6 = unembed ea cb a1 in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___6) + (fun uu___7 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___7 = unembed eb cb b1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___7) + (fun uu___8 -> + (fun b2 -> + let b2 = Obj.magic b2 in + let uu___8 = unembed ec cb c1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () (Obj.magic uu___8) + (fun uu___9 -> + (fun c2 -> + let c2 = + Obj.magic c2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2, c2))) + uu___9))) uu___8))) + uu___7))) + | uu___ -> + Obj.magic (Obj.repr FStar_Pervasives_Native.None)) + uu___) in mk_emb em1 un1 (fun uu___ -> let uu___1 = @@ -1285,6 +1325,366 @@ let e_tuple3 : [FStar_Syntax_Syntax.U_zero; FStar_Syntax_Syntax.U_zero; FStar_Syntax_Syntax.U_zero] uu___1) etyp +let e_tuple4 : + 'a 'b 'c 'd . + 'a embedding -> + 'b embedding -> + 'c embedding -> 'd embedding -> ('a * 'b * 'c * 'd) embedding + = + fun ea -> + fun eb -> + fun ec -> + fun ed -> + let etyp uu___ = + let uu___1 = + let uu___2 = + FStar_Ident.string_of_lid FStar_Parser_Const.lid_tuple4 in + let uu___3 = + let uu___4 = ea.e_typ () in + let uu___5 = + let uu___6 = eb.e_typ () in + let uu___7 = + let uu___8 = ec.e_typ () in + let uu___9 = let uu___10 = ed.e_typ () in [uu___10] in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + (uu___2, uu___3) in + FStar_Syntax_Syntax.ET_app uu___1 in + let em1 cb uu___ = + match uu___ with + | (x1, x2, x3, x4) -> + lazy_embed etyp (x1, x2, x3, x4) + (fun uu___1 -> + let uu___2 = + let uu___3 = + let uu___4 = embed ed cb x4 in as_arg uu___4 in + let uu___4 = + let uu___5 = + let uu___6 = embed ec cb x3 in as_arg uu___6 in + let uu___6 = + let uu___7 = + let uu___8 = embed eb cb x2 in as_arg uu___8 in + let uu___8 = + let uu___9 = + let uu___10 = embed ea cb x1 in as_arg uu___10 in + let uu___10 = + let uu___11 = + let uu___12 = type_of ed in as_iarg uu___12 in + let uu___12 = + let uu___13 = + let uu___14 = type_of ec in + as_iarg uu___14 in + let uu___14 = + let uu___15 = + let uu___16 = type_of eb in + as_iarg uu___16 in + let uu___16 = + let uu___17 = + let uu___18 = type_of ea in + as_iarg uu___18 in + [uu___17] in + uu___15 :: uu___16 in + uu___13 :: uu___14 in + uu___11 :: uu___12 in + uu___9 :: uu___10 in + uu___7 :: uu___8 in + uu___5 :: uu___6 in + uu___3 :: uu___4 in + lid_as_constr FStar_Parser_Const.lid_Mktuple4 + [FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero] uu___2) in + let un1 cb trm = + lazy_unembed etyp trm + (fun uu___ -> + (fun trm1 -> + match trm1.nbe_t with + | Construct + (fvar, us, + (d1, uu___)::(c1, uu___1)::(b1, uu___2)::(a1, + uu___3)::uu___4::uu___5::uu___6::uu___7::[]) + when + FStar_Syntax_Syntax.fv_eq_lid fvar + FStar_Parser_Const.lid_Mktuple4 + -> + Obj.magic + (Obj.repr + (let uu___8 = unembed ea cb a1 in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___8) + (fun uu___9 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___9 = unembed eb cb b1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () + () (Obj.magic uu___9) + (fun uu___10 -> + (fun b2 -> + let b2 = Obj.magic b2 in + let uu___10 = + unembed ec cb c1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___10) + (fun uu___11 -> + (fun c2 -> + let c2 = + Obj.magic c2 in + let uu___11 = + unembed ed cb + d1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___11) + (fun uu___12 + -> + (fun d2 + -> + let d2 = + Obj.magic + d2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2, + c2, d2))) + uu___12))) + uu___11))) uu___10))) + uu___9))) + | uu___ -> + Obj.magic (Obj.repr FStar_Pervasives_Native.None)) + uu___) in + mk_emb em1 un1 + (fun uu___ -> + let uu___1 = + let uu___2 = let uu___3 = type_of ed in as_arg uu___3 in + let uu___3 = + let uu___4 = let uu___5 = type_of ec in as_arg uu___5 in + let uu___5 = + let uu___6 = let uu___7 = type_of eb in as_arg uu___7 in + let uu___7 = + let uu___8 = let uu___9 = type_of ea in as_arg uu___9 in + [uu___8] in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + uu___2 :: uu___3 in + lid_as_typ FStar_Parser_Const.lid_tuple4 + [FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero] uu___1) etyp +let e_tuple5 : + 'a 'b 'c 'd 'e . + 'a embedding -> + 'b embedding -> + 'c embedding -> + 'd embedding -> 'e embedding -> ('a * 'b * 'c * 'd * 'e) embedding + = + fun ea -> + fun eb -> + fun ec -> + fun ed -> + fun ee -> + let etyp uu___ = + let uu___1 = + let uu___2 = + FStar_Ident.string_of_lid FStar_Parser_Const.lid_tuple5 in + let uu___3 = + let uu___4 = ea.e_typ () in + let uu___5 = + let uu___6 = eb.e_typ () in + let uu___7 = + let uu___8 = ec.e_typ () in + let uu___9 = + let uu___10 = ed.e_typ () in + let uu___11 = let uu___12 = ee.e_typ () in [uu___12] in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + (uu___2, uu___3) in + FStar_Syntax_Syntax.ET_app uu___1 in + let em1 cb uu___ = + match uu___ with + | (x1, x2, x3, x4, x5) -> + lazy_embed etyp (x1, x2, x3, x4, x5) + (fun uu___1 -> + let uu___2 = + let uu___3 = + let uu___4 = embed ee cb x5 in as_arg uu___4 in + let uu___4 = + let uu___5 = + let uu___6 = embed ed cb x4 in as_arg uu___6 in + let uu___6 = + let uu___7 = + let uu___8 = embed ec cb x3 in as_arg uu___8 in + let uu___8 = + let uu___9 = + let uu___10 = embed eb cb x2 in + as_arg uu___10 in + let uu___10 = + let uu___11 = + let uu___12 = embed ea cb x1 in + as_arg uu___12 in + let uu___12 = + let uu___13 = + let uu___14 = type_of ee in + as_iarg uu___14 in + let uu___14 = + let uu___15 = + let uu___16 = type_of ed in + as_iarg uu___16 in + let uu___16 = + let uu___17 = + let uu___18 = type_of ec in + as_iarg uu___18 in + let uu___18 = + let uu___19 = + let uu___20 = type_of eb in + as_iarg uu___20 in + let uu___20 = + let uu___21 = + let uu___22 = type_of ea in + as_iarg uu___22 in + [uu___21] in + uu___19 :: uu___20 in + uu___17 :: uu___18 in + uu___15 :: uu___16 in + uu___13 :: uu___14 in + uu___11 :: uu___12 in + uu___9 :: uu___10 in + uu___7 :: uu___8 in + uu___5 :: uu___6 in + uu___3 :: uu___4 in + lid_as_constr FStar_Parser_Const.lid_Mktuple5 + [FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero] uu___2) in + let un1 cb trm = + lazy_unembed etyp trm + (fun uu___ -> + (fun trm1 -> + match trm1.nbe_t with + | Construct + (fvar, us, + (e1, uu___)::(d1, uu___1)::(c1, uu___2)::(b1, + uu___3):: + (a1, uu___4)::uu___5::uu___6::uu___7::uu___8::uu___9::[]) + when + FStar_Syntax_Syntax.fv_eq_lid fvar + FStar_Parser_Const.lid_Mktuple5 + -> + Obj.magic + (Obj.repr + (let uu___10 = unembed ea cb a1 in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option () () + (Obj.magic uu___10) + (fun uu___11 -> + (fun a2 -> + let a2 = Obj.magic a2 in + let uu___11 = unembed eb cb b1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () (Obj.magic uu___11) + (fun uu___12 -> + (fun b2 -> + let b2 = Obj.magic b2 in + let uu___12 = + unembed ec cb c1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___12) + (fun uu___13 -> + (fun c2 -> + let c2 = + Obj.magic c2 in + let uu___13 = + unembed ed cb + d1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___13) + (fun + uu___14 + -> + (fun d2 + -> + let d2 = + Obj.magic + d2 in + let uu___14 + = + unembed + ee cb e1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___14) + (fun + uu___15 + -> + (fun e2 + -> + let e2 = + Obj.magic + e2 in + Obj.magic + (FStar_Pervasives_Native.Some + (a2, b2, + c2, d2, + e2))) + uu___15))) + uu___14))) + uu___13))) + uu___12))) uu___11))) + | uu___ -> + Obj.magic (Obj.repr FStar_Pervasives_Native.None)) + uu___) in + mk_emb em1 un1 + (fun uu___ -> + let uu___1 = + let uu___2 = let uu___3 = type_of ee in as_arg uu___3 in + let uu___3 = + let uu___4 = let uu___5 = type_of ed in as_arg uu___5 in + let uu___5 = + let uu___6 = let uu___7 = type_of ec in as_arg uu___7 in + let uu___7 = + let uu___8 = + let uu___9 = type_of eb in as_arg uu___9 in + let uu___9 = + let uu___10 = + let uu___11 = type_of ea in as_arg uu___11 in + [uu___10] in + uu___8 :: uu___9 in + uu___6 :: uu___7 in + uu___4 :: uu___5 in + uu___2 :: uu___3 in + lid_as_typ FStar_Parser_Const.lid_tuple5 + [FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero; + FStar_Syntax_Syntax.U_zero] uu___1) etyp let e_either : 'a 'b . 'a embedding -> @@ -1364,7 +1764,7 @@ let e_either : lid_as_typ FStar_Parser_Const.either_lid [FStar_Syntax_Syntax.U_zero; FStar_Syntax_Syntax.U_zero] uu___1) etyp -let (e_range : FStar_Compiler_Range_Type.range embedding) = +let (e___range : FStar_Compiler_Range_Type.range embedding) = let em1 cb r = Constant (Range r) in let un1 cb t1 = match t1 with @@ -1373,6 +1773,55 @@ let (e_range : FStar_Compiler_Range_Type.range embedding) = mk_emb' em1 un1 (fun uu___ -> lid_as_typ FStar_Parser_Const.__range_lid [] []) (FStar_Syntax_Embeddings_Base.emb_typ_of FStar_Syntax_Embeddings.e_range) +let e_sealed : 'a . 'a embedding -> 'a FStar_Compiler_Sealed.sealed embedding + = + fun ea -> + let etyp uu___ = + let uu___1 = + let uu___2 = FStar_Ident.string_of_lid FStar_Parser_Const.sealed_lid in + let uu___3 = let uu___4 = ea.e_typ () in [uu___4] in (uu___2, uu___3) in + FStar_Syntax_Syntax.ET_app uu___1 in + let em1 cb x = + lazy_embed etyp x + (fun uu___ -> + let uu___1 = + let uu___2 = + let uu___3 = embed ea cb (FStar_Compiler_Sealed.unseal x) in + as_arg uu___3 in + let uu___3 = + let uu___4 = let uu___5 = type_of ea in as_iarg uu___5 in + [uu___4] in + uu___2 :: uu___3 in + lid_as_constr FStar_Parser_Const.seal_lid + [FStar_Syntax_Syntax.U_zero] uu___1) in + let un1 cb trm = + lazy_unembed etyp trm + (fun uu___ -> + (fun trm1 -> + match trm1.nbe_t with + | Construct (fvar, us, (a1, uu___)::uu___1::[]) when + FStar_Syntax_Syntax.fv_eq_lid fvar + FStar_Parser_Const.seal_lid + -> + Obj.magic + (Obj.repr + (let uu___2 = unembed ea cb a1 in + FStar_Class_Monad.fmap FStar_Class_Monad.monad_option + () () + (fun uu___3 -> + (Obj.magic FStar_Compiler_Sealed.seal) uu___3) + (Obj.magic uu___2))) + | uu___ -> Obj.magic (Obj.repr FStar_Pervasives_Native.None)) + uu___) in + mk_emb em1 un1 + (fun uu___ -> + let uu___1 = + let uu___2 = let uu___3 = type_of ea in as_arg uu___3 in [uu___2] in + lid_as_typ FStar_Parser_Const.sealed_lid + [FStar_Syntax_Syntax.U_zero] uu___1) etyp +let (e_range : FStar_Compiler_Range_Type.range embedding) = + embed_as (e_sealed e___range) FStar_Compiler_Sealed.unseal + FStar_Compiler_Sealed.seal FStar_Pervasives_Native.None let (e_issue : FStar_Errors.issue embedding) = let t_issue = FStar_Syntax_Embeddings_Base.type_of FStar_Syntax_Embeddings.e_issue in @@ -1780,52 +2229,6 @@ let (e_norm_step : FStar_Pervasives.norm_step embedding) = mkFV uu___1 [] []) (FStar_Syntax_Embeddings_Base.emb_typ_of FStar_Syntax_Embeddings.e_norm_step) -let e_sealed : 'a . 'a embedding -> 'a FStar_Compiler_Sealed.sealed embedding - = - fun ea -> - let etyp uu___ = - let uu___1 = - let uu___2 = FStar_Ident.string_of_lid FStar_Parser_Const.sealed_lid in - let uu___3 = let uu___4 = ea.e_typ () in [uu___4] in (uu___2, uu___3) in - FStar_Syntax_Syntax.ET_app uu___1 in - let em1 cb x = - lazy_embed etyp x - (fun uu___ -> - let uu___1 = - let uu___2 = - let uu___3 = embed ea cb (FStar_Compiler_Sealed.unseal x) in - as_arg uu___3 in - let uu___3 = - let uu___4 = let uu___5 = type_of ea in as_iarg uu___5 in - [uu___4] in - uu___2 :: uu___3 in - lid_as_constr FStar_Parser_Const.seal_lid - [FStar_Syntax_Syntax.U_zero] uu___1) in - let un1 cb trm = - lazy_unembed etyp trm - (fun uu___ -> - (fun trm1 -> - match trm1.nbe_t with - | Construct (fvar, us, (a1, uu___)::uu___1::[]) when - FStar_Syntax_Syntax.fv_eq_lid fvar - FStar_Parser_Const.seal_lid - -> - Obj.magic - (Obj.repr - (let uu___2 = unembed ea cb a1 in - FStar_Class_Monad.fmap FStar_Class_Monad.monad_option - () () - (fun uu___3 -> - (Obj.magic FStar_Compiler_Sealed.seal) uu___3) - (Obj.magic uu___2))) - | uu___ -> Obj.magic (Obj.repr FStar_Pervasives_Native.None)) - uu___) in - mk_emb em1 un1 - (fun uu___ -> - let uu___1 = - let uu___2 = let uu___3 = type_of ea in as_arg uu___3 in [uu___2] in - lid_as_typ FStar_Parser_Const.sealed_lid - [FStar_Syntax_Syntax.U_zero] uu___1) etyp let (bogus_cbs : nbe_cbs) = { iapp = (fun h -> fun _args -> h); diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Range.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Range.ml index 426a3fb43ac..c00d5be9c3d 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Range.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Range.ml @@ -1,35 +1,122 @@ open Prims +type unsealedRange = + | U of FStar_Compiler_Range_Type.range +let (uu___is_U : unsealedRange -> Prims.bool) = fun projectee -> true +let (__proj__U__item___0 : unsealedRange -> FStar_Compiler_Range_Type.range) + = fun projectee -> match projectee with | U _0 -> _0 +let (mk_range : + Prims.string -> + FStar_BigInt.t -> + FStar_BigInt.t -> + FStar_BigInt.t -> FStar_BigInt.t -> FStar_Compiler_Range_Type.range) + = + fun fn -> + fun from_l -> + fun from_c -> + fun to_l -> + fun to_c -> + let uu___ = + let uu___1 = FStar_BigInt.to_int_fs from_l in + let uu___2 = FStar_BigInt.to_int_fs from_c in + FStar_Compiler_Range_Type.mk_pos uu___1 uu___2 in + let uu___1 = + let uu___2 = FStar_BigInt.to_int_fs to_l in + let uu___3 = FStar_BigInt.to_int_fs to_c in + FStar_Compiler_Range_Type.mk_pos uu___2 uu___3 in + FStar_Compiler_Range_Type.mk_range fn uu___ uu___1 +let (__mk_range : + Prims.string -> + FStar_BigInt.t -> + FStar_BigInt.t -> FStar_BigInt.t -> FStar_BigInt.t -> unsealedRange) + = + fun fn -> + fun from_l -> + fun from_c -> + fun to_l -> + fun to_c -> + let uu___ = mk_range fn from_l from_c to_l to_c in U uu___ +let (explode : + unsealedRange -> + (Prims.string * FStar_BigInt.t * FStar_BigInt.t * FStar_BigInt.t * + FStar_BigInt.t)) + = + fun r -> + match r with + | U r1 -> + let uu___ = FStar_Compiler_Range_Ops.file_of_range r1 in + let uu___1 = + let uu___2 = + let uu___3 = FStar_Compiler_Range_Ops.start_of_range r1 in + FStar_Compiler_Range_Ops.line_of_pos uu___3 in + FStar_BigInt.of_int_fs uu___2 in + let uu___2 = + let uu___3 = + let uu___4 = FStar_Compiler_Range_Ops.start_of_range r1 in + FStar_Compiler_Range_Ops.col_of_pos uu___4 in + FStar_BigInt.of_int_fs uu___3 in + let uu___3 = + let uu___4 = + let uu___5 = FStar_Compiler_Range_Ops.end_of_range r1 in + FStar_Compiler_Range_Ops.line_of_pos uu___5 in + FStar_BigInt.of_int_fs uu___4 in + let uu___4 = + let uu___5 = + let uu___6 = FStar_Compiler_Range_Ops.end_of_range r1 in + FStar_Compiler_Range_Ops.col_of_pos uu___6 in + FStar_BigInt.of_int_fs uu___5 in + (uu___, uu___1, uu___2, uu___3, uu___4) +let (e_unsealedRange : unsealedRange FStar_Syntax_Embeddings_Base.embedding) + = + FStar_Syntax_Embeddings_Base.embed_as FStar_Syntax_Embeddings.e___range + (fun r -> U r) (fun uu___ -> match uu___ with | U r -> r) + FStar_Pervasives_Native.None +let (nbe_e_unsealedRange : unsealedRange FStar_TypeChecker_NBETerm.embedding) + = + FStar_TypeChecker_NBETerm.embed_as FStar_TypeChecker_NBETerm.e___range + (fun r -> U r) (fun uu___ -> match uu___ with | U r -> r) + FStar_Pervasives_Native.None let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = let uu___ = FStar_TypeChecker_Primops_Base.mk5 Prims.int_zero - FStar_Parser_Const.mk_range_lid FStar_Syntax_Embeddings.e_string + FStar_Parser_Const.__mk_range_lid FStar_Syntax_Embeddings.e_string FStar_TypeChecker_NBETerm.e_string FStar_Syntax_Embeddings.e_int FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_int FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_int FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_int - FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_range - FStar_TypeChecker_NBETerm.e_range - (fun fn -> - fun from_l -> - fun from_c -> - fun to_l -> - fun to_c -> - let uu___1 = - let uu___2 = FStar_BigInt.to_int_fs from_l in - let uu___3 = FStar_BigInt.to_int_fs from_c in - FStar_Compiler_Range_Type.mk_pos uu___2 uu___3 in - let uu___2 = - let uu___3 = FStar_BigInt.to_int_fs to_l in - let uu___4 = FStar_BigInt.to_int_fs to_c in - FStar_Compiler_Range_Type.mk_pos uu___3 uu___4 in - FStar_Compiler_Range_Type.mk_range fn uu___1 uu___2) in + FStar_TypeChecker_NBETerm.e_int e_unsealedRange nbe_e_unsealedRange + __mk_range in let uu___1 = let uu___2 = - FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero - FStar_Parser_Const.join_range_lid FStar_Syntax_Embeddings.e_range - FStar_TypeChecker_NBETerm.e_range FStar_Syntax_Embeddings.e_range - FStar_TypeChecker_NBETerm.e_range FStar_Syntax_Embeddings.e_range - FStar_TypeChecker_NBETerm.e_range - FStar_Compiler_Range_Ops.union_ranges in - [uu___2] in + FStar_TypeChecker_Primops_Base.mk5 Prims.int_zero + FStar_Parser_Const.mk_range_lid FStar_Syntax_Embeddings.e_string + FStar_TypeChecker_NBETerm.e_string FStar_Syntax_Embeddings.e_int + FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_int + FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_int + FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_int + FStar_TypeChecker_NBETerm.e_int FStar_Syntax_Embeddings.e_range + FStar_TypeChecker_NBETerm.e_range mk_range in + let uu___3 = + let uu___4 = + FStar_TypeChecker_Primops_Base.mk1 Prims.int_zero + FStar_Parser_Const.__explode_range_lid e_unsealedRange + nbe_e_unsealedRange + (FStar_Syntax_Embeddings.e_tuple5 FStar_Syntax_Embeddings.e_string + FStar_Syntax_Embeddings.e_int FStar_Syntax_Embeddings.e_int + FStar_Syntax_Embeddings.e_int FStar_Syntax_Embeddings.e_int) + (FStar_TypeChecker_NBETerm.e_tuple5 + FStar_TypeChecker_NBETerm.e_string + FStar_TypeChecker_NBETerm.e_int FStar_TypeChecker_NBETerm.e_int + FStar_TypeChecker_NBETerm.e_int FStar_TypeChecker_NBETerm.e_int) + explode in + let uu___5 = + let uu___6 = + FStar_TypeChecker_Primops_Base.mk2 Prims.int_zero + FStar_Parser_Const.join_range_lid FStar_Syntax_Embeddings.e_range + FStar_TypeChecker_NBETerm.e_range FStar_Syntax_Embeddings.e_range + FStar_TypeChecker_NBETerm.e_range FStar_Syntax_Embeddings.e_range + FStar_TypeChecker_NBETerm.e_range + FStar_Compiler_Range_Ops.union_ranges 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/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index 33735b1298c..a091a3d7748 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/src/parser/FStar.Parser.Const.fst @@ -316,6 +316,8 @@ let __range_lid = p2l ["FStar"; "Range"; "__range"] let range_lid = p2l ["FStar"; "Range"; "range"] (* this is a sealed version of the above *) let range_0 = p2l ["FStar"; "Range"; "range_0"] let mk_range_lid = p2l ["FStar"; "Range"; "mk_range"] +let __mk_range_lid = p2l ["FStar"; "Range"; "__mk_range"] +let __explode_range_lid = p2l ["FStar"; "Range"; "explode"] let join_range_lid = p2l ["FStar"; "Range"; "join_range"] let guard_free = pconst "guard_free" @@ -432,6 +434,8 @@ let mk_tuple_lid n r = let lid_tuple2 = mk_tuple_lid 2 dummyRange let lid_tuple3 = mk_tuple_lid 3 dummyRange +let lid_tuple4 = mk_tuple_lid 4 dummyRange +let lid_tuple5 = mk_tuple_lid 5 dummyRange let is_tuple_constructor_string (s:string) :bool = U.starts_with s "FStar.Pervasives.Native.tuple" @@ -445,6 +449,8 @@ let mk_tuple_data_lid n r = let lid_Mktuple2 = mk_tuple_data_lid 2 dummyRange let lid_Mktuple3 = mk_tuple_data_lid 3 dummyRange +let lid_Mktuple4 = mk_tuple_data_lid 4 dummyRange +let lid_Mktuple5 = mk_tuple_data_lid 5 dummyRange let is_tuple_datacon_string (s:string) :bool = U.starts_with s "FStar.Pervasives.Native.Mktuple" diff --git a/src/syntax/FStar.Syntax.Embeddings.fst b/src/syntax/FStar.Syntax.Embeddings.fst index 4b770a8163d..1525bcc847a 100644 --- a/src/syntax/FStar.Syntax.Embeddings.fst +++ b/src/syntax/FStar.Syntax.Embeddings.fst @@ -381,7 +381,7 @@ let e_option (ea : embedding 'a) : Tot _ = let e_tuple2 (ea:embedding 'a) (eb:embedding 'b) = let typ () = S.t_tuple2_of (type_of ea) (type_of eb) in - let emb_t_pair_a_b () = + let emb_t_pair () = ET_app(PC.lid_tuple2 |> Ident.string_of_lid, [emb_typ_of 'a (); emb_typ_of 'b ()]) in let printer (x, y) = @@ -390,7 +390,7 @@ let e_tuple2 (ea:embedding 'a) (eb:embedding 'b) = let em (x:('a & 'b)) (rng:range) shadow norm : term = lazy_embed printer - emb_t_pair_a_b + emb_t_pair rng typ x @@ -416,16 +416,17 @@ let e_tuple2 (ea:embedding 'a) (eb:embedding 'b) = let un (t:term) norm : option ('a & 'b) = lazy_unembed printer - emb_t_pair_a_b + emb_t_pair t typ (fun t -> let hd, args = U.head_and_args_full t in match (U.un_uinst hd).n, args with | Tm_fvar fv, [_; _; (a, _); (b, _)] when S.fv_eq_lid fv PC.lid_Mktuple2 -> - BU.bind_opt (try_unembed a norm) (fun a -> - BU.bind_opt (try_unembed b norm) (fun b -> - Some (a, b))) + let open FStar.Class.Monad in + let! a = try_unembed a norm in + let! b = try_unembed b norm in + Some (a, b) | _ -> None) in mk_emb_full @@ -433,11 +434,11 @@ let e_tuple2 (ea:embedding 'a) (eb:embedding 'b) = un typ printer - emb_t_pair_a_b + emb_t_pair let e_tuple3 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) = let typ () = S.t_tuple3_of (type_of ea) (type_of eb) (type_of ec) in - let emb_t_pair_a_b_c () = + let emb_t_pair () = ET_app(PC.lid_tuple3 |> Ident.string_of_lid, [emb_typ_of 'a (); emb_typ_of 'b (); emb_typ_of 'c ()]) in let printer (x, y, z) = @@ -446,7 +447,7 @@ let e_tuple3 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) = let em ((x1, x2, x3):('a & 'b & 'c)) (rng:range) shadow norm : term = lazy_embed printer - emb_t_pair_a_b_c + emb_t_pair rng typ (x1, x2, x3) @@ -476,17 +477,157 @@ let e_tuple3 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) = let un (t:term) norm : option ('a & 'b & 'c) = lazy_unembed printer - emb_t_pair_a_b_c + emb_t_pair t typ (fun t -> let hd, args = U.head_and_args_full t in match (U.un_uinst hd).n, args with | Tm_fvar fv, [_; _; _; (a, _); (b, _); (c, _)] when S.fv_eq_lid fv PC.lid_Mktuple3 -> - BU.bind_opt (try_unembed a norm) (fun a -> - BU.bind_opt (try_unembed b norm) (fun b -> - BU.bind_opt (try_unembed c norm) (fun c -> - Some (a, b, c)))) + let open FStar.Class.Monad in + let! a = try_unembed a norm in + let! b = try_unembed b norm in + let! c = try_unembed c norm in + Some (a, b, c) + | _ -> None) + in + mk_emb_full + em + un + typ + printer + emb_t_pair + +let e_tuple4 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) (ed:embedding 'd) = + let typ () = S.t_tuple4_of (type_of ea) (type_of eb) (type_of ec) (type_of ed) in + let emb_t_pair () = + ET_app(PC.lid_tuple4 |> Ident.string_of_lid, [emb_typ_of 'a (); emb_typ_of 'b (); emb_typ_of 'c (); emb_typ_of 'd ()]) + in + let printer (x, y, z, w) = + BU.format4 "(%s, %s, %s, %s)" (printer_of ea x) (printer_of eb y) (printer_of ec z) (printer_of ed w) + in + let em (x1, x2, x3, x4) (rng:range) shadow norm : term = + lazy_embed + printer + emb_t_pair + rng + typ + (x1, x2, x3, x4) + (fun () -> + let proj i abcd = + let proj_i = U.mk_field_projector_name (PC.mk_tuple_data_lid 4 rng) (S.null_bv S.tun) i in + let proj_i_tm = S.fv_to_tm (lid_as_fv proj_i None) in + S.mk_Tm_app (S.mk_Tm_uinst proj_i_tm [U_zero]) + [S.iarg (type_of ea); + S.iarg (type_of eb); + S.iarg (type_of ec); + S.iarg (type_of ed); + S.as_arg abcd] // abc == shadow + rng + in + let shadow_a = map_shadow shadow (proj 1) in + let shadow_b = map_shadow shadow (proj 2) in + let shadow_c = map_shadow shadow (proj 3) in + let shadow_d = map_shadow shadow (proj 4) in + S.mk_Tm_app (S.mk_Tm_uinst (S.tdataconstr PC.lid_Mktuple4) [U_zero;U_zero;U_zero;U_zero]) + [S.iarg (type_of ea); + S.iarg (type_of eb); + S.iarg (type_of ec); + S.iarg (type_of ed); + S.as_arg (embed x1 rng shadow_a norm); + S.as_arg (embed x2 rng shadow_b norm); + S.as_arg (embed x3 rng shadow_c norm); + S.as_arg (embed x4 rng shadow_d norm)] + rng) + in + let un (t:term) norm : option ('a & 'b & 'c & 'd) = + lazy_unembed + printer + emb_t_pair + t + typ + (fun t -> + let hd, args = U.head_and_args_full t in + match (U.un_uinst hd).n, args with + | Tm_fvar fv, [_; _; _; _; (a, _); (b, _); (c, _); (d, _)] when S.fv_eq_lid fv PC.lid_Mktuple4 -> + let open FStar.Class.Monad in + let! a = try_unembed a norm in + let! b = try_unembed b norm in + let! c = try_unembed c norm in + let! d = try_unembed d norm in + Some (a, b, c, d) + | _ -> None) + in + mk_emb_full + em + un + typ + printer + emb_t_pair + +let e_tuple5 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) (ed:embedding 'd) (ee:embedding 'e) = + let typ () = S.t_tuple5_of (type_of ea) (type_of eb) (type_of ec) (type_of ed) (type_of ee) in + let emb_t_pair () = + ET_app(PC.lid_tuple5 |> Ident.string_of_lid, [emb_typ_of 'a (); emb_typ_of 'b (); emb_typ_of 'c (); emb_typ_of 'd (); emb_typ_of 'e ()]) + in + let printer (x, y, z, w, v) = + BU.format5 "(%s, %s, %s, %s, %s)" (printer_of ea x) (printer_of eb y) (printer_of ec z) (printer_of ed w) (printer_of ee v) + in + let em (x1, x2, x3, x4, x5) (rng:range) shadow norm : term = + lazy_embed + printer + emb_t_pair + rng + typ + (x1, x2, x3, x4, x5) + (fun () -> + let proj i abcde = + let proj_i = U.mk_field_projector_name (PC.mk_tuple_data_lid 5 rng) (S.null_bv S.tun) i in + let proj_i_tm = S.fv_to_tm (lid_as_fv proj_i None) in + S.mk_Tm_app (S.mk_Tm_uinst proj_i_tm [U_zero]) + [S.iarg (type_of ea); + S.iarg (type_of eb); + S.iarg (type_of ec); + S.iarg (type_of ed); + S.iarg (type_of ee); + S.as_arg abcde] // abc == shadow + rng + in + let shadow_a = map_shadow shadow (proj 1) in + let shadow_b = map_shadow shadow (proj 2) in + let shadow_c = map_shadow shadow (proj 3) in + let shadow_d = map_shadow shadow (proj 4) in + let shadow_e = map_shadow shadow (proj 5) in + S.mk_Tm_app (S.mk_Tm_uinst (S.tdataconstr PC.lid_Mktuple5) [U_zero;U_zero;U_zero;U_zero;U_zero]) + [S.iarg (type_of ea); + S.iarg (type_of eb); + S.iarg (type_of ec); + S.iarg (type_of ed); + S.iarg (type_of ee); + S.as_arg (embed x1 rng shadow_a norm); + S.as_arg (embed x2 rng shadow_b norm); + S.as_arg (embed x3 rng shadow_c norm); + S.as_arg (embed x4 rng shadow_d norm); + S.as_arg (embed x5 rng shadow_e norm)] + rng) + in + let un (t:term) norm : option ('a & 'b & 'c & 'd & 'e) = + lazy_unembed + printer + emb_t_pair + t + typ + (fun t -> + let hd, args = U.head_and_args_full t in + match (U.un_uinst hd).n, args with + | Tm_fvar fv, [_; _; _; _; _; (a, _); (b, _); (c, _); (d, _); (e, _)] when S.fv_eq_lid fv PC.lid_Mktuple5 -> + let open FStar.Class.Monad in + let! a = try_unembed a norm in + let! b = try_unembed b norm in + let! c = try_unembed c norm in + let! d = try_unembed d norm in + let! e = try_unembed e norm in + Some (a, b, c, d, e) | _ -> None) in mk_emb_full @@ -494,7 +635,7 @@ let e_tuple3 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) = un typ printer - emb_t_pair_a_b_c + emb_t_pair let e_either (ea:embedding 'a) (eb:embedding 'b) = let typ () = S.t_either_of (type_of ea) (type_of eb) in diff --git a/src/syntax/FStar.Syntax.Embeddings.fsti b/src/syntax/FStar.Syntax.Embeddings.fsti index 9c75763382d..940a1d5bb0a 100644 --- a/src/syntax/FStar.Syntax.Embeddings.fsti +++ b/src/syntax/FStar.Syntax.Embeddings.fsti @@ -50,6 +50,8 @@ instance val e_option : embedding 'a -> Tot (embedding (option 'a)) instance val e_list : embedding 'a -> Tot (embedding (list 'a)) instance val e_tuple2 : embedding 'a -> embedding 'b -> Tot (embedding ('a & 'b)) instance val e_tuple3 : embedding 'a -> embedding 'b -> embedding 'c -> Tot (embedding ('a & 'b & 'c)) +instance val e_tuple4 : embedding 'a -> embedding 'b -> embedding 'c -> embedding 'd -> Tot (embedding ('a & 'b & 'c & 'd)) +instance val e_tuple5 : embedding 'a -> embedding 'b -> embedding 'c -> embedding 'd -> embedding 'e -> Tot (embedding ('a & 'b & 'c & 'd & 'e)) instance val e_either : embedding 'a -> embedding 'b -> Tot (embedding (either 'a 'b)) instance val e_string_list : embedding (list string) val e_arrow : embedding 'a -> embedding 'b -> Tot (embedding ('a -> 'b)) diff --git a/src/syntax/FStar.Syntax.Syntax.fst b/src/syntax/FStar.Syntax.Syntax.fst index aec1ea5f637..5a3e44a5070 100644 --- a/src/syntax/FStar.Syntax.Syntax.fst +++ b/src/syntax/FStar.Syntax.Syntax.fst @@ -487,6 +487,14 @@ let t_tuple3_of t1 t2 t3 = mk_Tm_app (mk_Tm_uinst (tabbrev PC.lid_tuple3) [U_zero;U_zero;U_zero]) [as_arg t1; as_arg t2; as_arg t3] Range.dummyRange +let t_tuple4_of t1 t2 t3 t4 = mk_Tm_app + (mk_Tm_uinst (tabbrev PC.lid_tuple4) [U_zero;U_zero;U_zero;U_zero]) + [as_arg t1; as_arg t2; as_arg t3; as_arg t4] + Range.dummyRange +let t_tuple5_of t1 t2 t3 t4 t5 = mk_Tm_app + (mk_Tm_uinst (tabbrev PC.lid_tuple5) [U_zero;U_zero;U_zero;U_zero;U_zero]) + [as_arg t1; as_arg t2; as_arg t3; as_arg t4; as_arg t5] + Range.dummyRange let t_either_of t1 t2 = mk_Tm_app (mk_Tm_uinst (tabbrev PC.either_lid) [U_zero;U_zero]) [as_arg t1; as_arg t2] diff --git a/src/syntax/FStar.Syntax.Syntax.fsti b/src/syntax/FStar.Syntax.Syntax.fsti index 16346fcd192..04ad049cb58 100644 --- a/src/syntax/FStar.Syntax.Syntax.fsti +++ b/src/syntax/FStar.Syntax.Syntax.fsti @@ -909,6 +909,8 @@ val t_list_of : term -> term val t_option_of : term -> term val t_tuple2_of : term -> term -> term val t_tuple3_of : term -> term -> term -> term +val t_tuple4_of : term -> term -> term -> term -> term +val t_tuple5_of : term -> term -> term -> term -> term -> term val t_either_of : term -> term -> term val t_sealed_of : term -> term val t_erased_of : term -> term diff --git a/src/typechecker/FStar.TypeChecker.NBE.fst b/src/typechecker/FStar.TypeChecker.NBE.fst index 43737c7f16e..faf731435b2 100644 --- a/src/typechecker/FStar.TypeChecker.NBE.fst +++ b/src/typechecker/FStar.TypeChecker.NBE.fst @@ -853,17 +853,30 @@ and iapp (cfg : config) (f:t) (args:args) : t = end | Constant (SConst FStar.Const.Const_range_of) -> + let callbacks = { + iapp = iapp cfg; + translate = translate cfg []; + } in begin match args with - | [(a, _)] -> mk_rt a.nbe_r (Constant (Range a.nbe_r)) + | [(a, _)] -> + embed e_range callbacks a.nbe_r + // mk_rt a.nbe_r (Constant (Range a.nbe_r)) | _ -> failwith ("NBE ill-typed application Const_range_of: " ^ t_to_string f) end | Constant (SConst FStar.Const.Const_set_range_of) -> begin + let callbacks = { + iapp = iapp cfg; + translate = translate cfg []; + } in match args with - | [(t, _); ({nbe_t=Constant (Range r)}, _)] -> - { t with nbe_r = r} + | [(t, _); (r, _)] -> ( + match unembed e_range callbacks r with + | Some rr -> { t with nbe_r = rr } + | None -> magic() + ) | _ -> failwith ("NBE ill-typed application Const_set_range_of: " ^ t_to_string f) end @@ -1230,7 +1243,7 @@ and readback (cfg:config) (x:t) : term = | Constant (Int i) -> with_range (U.exp_int (Z.string_of_big_int i)) | Constant (String (s, r)) -> mk (S.Tm_constant (C.Const_string (s, r))) | Constant (Char c) -> with_range (U.exp_char c) - | Constant (Range r) -> PO.embed_simple x.nbe_r r + | Constant (Range r) -> PO.embed_simple #_ #EMB.e___range x.nbe_r r | Constant (Real r) -> PO.embed_simple x.nbe_r (Compiler.Real.Real r) | Constant (SConst c) -> mk (S.Tm_constant c) diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fst b/src/typechecker/FStar.TypeChecker.NBETerm.fst index 06d4723e62d..7c82ab72ba0 100644 --- a/src/typechecker/FStar.TypeChecker.NBETerm.fst +++ b/src/typechecker/FStar.TypeChecker.NBETerm.fst @@ -429,9 +429,10 @@ let e_tuple2 (ea:embedding 'a) (eb:embedding 'b) = lazy_unembed etyp trm (fun trm -> match trm.nbe_t with | Construct (fvar, us, [(b, _); (a, _); _; _]) when S.fv_eq_lid fvar PC.lid_Mktuple2 -> - BU.bind_opt (unembed ea cb a) (fun a -> - BU.bind_opt (unembed eb cb b) (fun b -> - Some (a, b))) + let open FStar.Class.Monad in + let! a = unembed ea cb a in + let! b = unembed eb cb b in + Some (a, b) | _ -> None) in mk_emb em un @@ -456,15 +457,83 @@ let e_tuple3 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) = let un cb (trm:t) : option ('a & 'b & 'c) = lazy_unembed etyp trm (fun trm -> match trm.nbe_t with - | Construct (fvar, us, [(c, _); (b, _); (a, _); _; _]) when S.fv_eq_lid fvar PC.lid_Mktuple3 -> - BU.bind_opt (unembed ea cb a) (fun a -> - BU.bind_opt (unembed eb cb b) (fun b -> - BU.bind_opt (unembed ec cb c) (fun c -> - Some (a, b, c)))) + | Construct (fvar, us, [(c, _); (b, _); (a, _); _; _; _]) when S.fv_eq_lid fvar PC.lid_Mktuple3 -> + let open FStar.Class.Monad in + let! a = unembed ea cb a in + let! b = unembed eb cb b in + let! c = unembed ec cb c in + Some (a, b, c) | _ -> None) in mk_emb em un (fun () -> lid_as_typ PC.lid_tuple3 [U_zero;U_zero;U_zero] [as_arg (type_of ec); as_arg (type_of eb); as_arg (type_of ea)]) etyp +let e_tuple4 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) (ed:embedding 'd) = + let etyp () = + ET_app(PC.lid_tuple4 |> Ident.string_of_lid, [ea.e_typ (); eb.e_typ (); ec.e_typ (); ed.e_typ ()]) + in + let em cb (x1, x2, x3, x4) : t = + lazy_embed etyp (x1, x2, x3, x4) (fun () -> + lid_as_constr (PC.lid_Mktuple4) + [U_zero; U_zero; U_zero; U_zero] + [as_arg (embed ed cb x4); + as_arg (embed ec cb x3); + as_arg (embed eb cb x2); + as_arg (embed ea cb x1); + as_iarg (type_of ed); + as_iarg (type_of ec); + as_iarg (type_of eb); + as_iarg (type_of ea)]) + in + let un cb (trm:t) : option ('a & 'b & 'c & 'd) = + lazy_unembed etyp trm (fun trm -> + match trm.nbe_t with + | Construct (fvar, us, [(d, _); (c, _); (b, _); (a, _); _; _; _; _]) when S.fv_eq_lid fvar PC.lid_Mktuple4 -> + let open FStar.Class.Monad in + let! a = unembed ea cb a in + let! b = unembed eb cb b in + let! c = unembed ec cb c in + let! d = unembed ed cb d in + Some (a, b, c, d) + | _ -> None) + in + mk_emb em un (fun () -> lid_as_typ PC.lid_tuple4 [U_zero;U_zero;U_zero;U_zero] [as_arg (type_of ed); as_arg (type_of ec); as_arg (type_of eb); as_arg (type_of ea)]) etyp + +let e_tuple5 (ea:embedding 'a) (eb:embedding 'b) (ec:embedding 'c) (ed:embedding 'd) (ee:embedding 'e) = + let etyp () = + ET_app(PC.lid_tuple5 |> Ident.string_of_lid, [ea.e_typ (); eb.e_typ (); ec.e_typ (); ed.e_typ (); ee.e_typ ()]) + in + let em cb (x1, x2, x3, x4, x5) : t = + lazy_embed etyp (x1, x2, x3, x4, x5) (fun () -> + lid_as_constr (PC.lid_Mktuple5) + [U_zero; U_zero; U_zero; U_zero;U_zero] + [as_arg (embed ee cb x5); + as_arg (embed ed cb x4); + as_arg (embed ec cb x3); + as_arg (embed eb cb x2); + as_arg (embed ea cb x1); + as_iarg (type_of ee); + as_iarg (type_of ed); + as_iarg (type_of ec); + as_iarg (type_of eb); + as_iarg (type_of ea)]) + in + let un cb (trm:t) : option ('a & 'b & 'c & 'd & 'e) = + lazy_unembed etyp trm (fun trm -> + match trm.nbe_t with + | Construct (fvar, us, [(e, _); (d, _); (c, _); (b, _); (a, _); _; _; _; _; _]) when S.fv_eq_lid fvar PC.lid_Mktuple5 -> + let open FStar.Class.Monad in + let! a = unembed ea cb a in + let! b = unembed eb cb b in + let! c = unembed ec cb c in + let! d = unembed ed cb d in + let! e = unembed ee cb e in + Some (a, b, c, d, e) + | _ -> None) + in + mk_emb em un + (fun () -> lid_as_typ PC.lid_tuple5 [U_zero;U_zero;U_zero;U_zero;U_zero] [as_arg (type_of ee); as_arg (type_of ed); as_arg (type_of ec); as_arg (type_of eb); as_arg (type_of ea)]) + etyp + let e_either (ea:embedding 'a) (eb:embedding 'b) = let etyp () = ET_app(PC.either_lid |> Ident.string_of_lid, [ea.e_typ (); eb.e_typ ()]) @@ -498,8 +567,8 @@ let e_either (ea:embedding 'a) (eb:embedding 'b) = in mk_emb em un (fun () -> lid_as_typ PC.either_lid [U_zero;U_zero] [as_arg (type_of eb); as_arg (type_of ea)]) etyp -// Embedding range -let e_range : embedding Range.range = +// Embedding range (unsealed) +let e___range : embedding Range.range = let em cb r = Constant (Range r) in let un cb t = match t with @@ -509,6 +578,29 @@ let e_range : embedding Range.range = in mk_emb' em un (fun () -> lid_as_typ PC.__range_lid [] []) (SE.emb_typ_of Range.range) +// Embedding a sealed term. This just calls the embedding for a but also +// adds a `seal` marker to the result. The unembedding removes it. +let e_sealed (ea : embedding 'a) : Prims.Tot (embedding (Sealed.sealed 'a)) = + let etyp () = + ET_app(PC.sealed_lid |> Ident.string_of_lid, [ea.e_typ ()]) + in + let em cb (x: Sealed.sealed 'a) : t = + lazy_embed etyp x (fun () -> + lid_as_constr PC.seal_lid [U_zero] [as_arg (embed ea cb (Sealed.unseal x)); + as_iarg (type_of ea)]) + in + let un cb (trm:t) : option (Sealed.sealed 'a) = + lazy_unembed etyp trm (fun trm -> + match trm.nbe_t with + | Construct (fvar, us, [(a, _); _]) when S.fv_eq_lid fvar PC.seal_lid -> + Class.Monad.fmap Sealed.seal <| unembed ea cb a + | _ -> None) + in + mk_emb em un (fun () -> lid_as_typ PC.sealed_lid [U_zero] [as_arg (type_of ea)]) etyp + +let e_range : embedding Range.range = + embed_as (e_sealed e___range) Sealed.unseal Sealed.seal None + let e_issue : embedding FStar.Errors.issue = let t_issue = SE.type_of SE.e_issue in let li blob rng = { blob=Dyn.mkdyn blob; lkind = Lazy_issue; ltyp = t_issue; rng } in @@ -673,26 +765,6 @@ let e_norm_step = mk_emb em un (fun () -> mkFV (lid_as_fv PC.norm_step_lid None) [] []) (SE.emb_typ_of norm_step) -// Embedding a sealed term. This just calls the embedding for a but also -// adds a `seal` marker to the result. The unembedding removes it. -let e_sealed (ea : embedding 'a) : Prims.Tot (embedding (Sealed.sealed 'a)) = - let etyp () = - ET_app(PC.sealed_lid |> Ident.string_of_lid, [ea.e_typ ()]) - in - let em cb (x: Sealed.sealed 'a) : t = - lazy_embed etyp x (fun () -> - lid_as_constr PC.seal_lid [U_zero] [as_arg (embed ea cb (Sealed.unseal x)); - as_iarg (type_of ea)]) - in - let un cb (trm:t) : option (Sealed.sealed 'a) = - lazy_unembed etyp trm (fun trm -> - match trm.nbe_t with - | Construct (fvar, us, [(a, _); _]) when S.fv_eq_lid fvar PC.seal_lid -> - Class.Monad.fmap Sealed.seal <| unembed ea cb a - | _ -> None) - in - mk_emb em un (fun () -> lid_as_typ PC.sealed_lid [U_zero] [as_arg (type_of ea)]) etyp - (* Interface for building primitive steps *) let bogus_cbs = { diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fsti b/src/typechecker/FStar.TypeChecker.NBETerm.fsti index 853febc6457..f649a8016c9 100644 --- a/src/typechecker/FStar.TypeChecker.NBETerm.fsti +++ b/src/typechecker/FStar.TypeChecker.NBETerm.fsti @@ -283,7 +283,8 @@ instance val e_real : embedding Compiler.Real.real instance val e_unit : embedding unit val e_any : embedding t val mk_any_emb : t -> embedding t -instance val e_range : embedding Range.range +val e___range : embedding Range.range (* unsealed *) +instance val e_range : embedding Range.range (* sealed *) instance val e_issue : embedding FStar.Errors.issue instance val e_document : embedding FStar.Pprint.document instance val e_vconfig : embedding vconfig @@ -292,6 +293,8 @@ instance val e_list : #a:Type -> embedding a -> Prims.Tot (embedding (list a)) instance val e_option : embedding 'a -> Prims.Tot (embedding (option 'a)) instance val e_tuple2 : embedding 'a -> embedding 'b -> Prims.Tot (embedding ('a & 'b)) instance val e_tuple3 : embedding 'a -> embedding 'b -> embedding 'c -> Prims.Tot (embedding ('a & 'b & 'c)) +instance val e_tuple4 : embedding 'a -> embedding 'b -> embedding 'c -> embedding 'd -> Prims.Tot (embedding ('a & 'b & 'c & 'd)) +instance val e_tuple5 : embedding 'a -> embedding 'b -> embedding 'c -> embedding 'd -> embedding 'e -> Prims.Tot (embedding ('a & 'b & 'c & 'd & 'e)) instance val e_either : embedding 'a -> embedding 'b -> Prims.Tot (embedding (either 'a 'b)) instance val e_sealed : embedding 'a -> Prims.Tot (embedding (FStar.Compiler.Sealed.sealed 'a)) instance val e_string_list : embedding (list string) diff --git a/src/typechecker/FStar.TypeChecker.Primops.Range.fst b/src/typechecker/FStar.TypeChecker.Primops.Range.fst index d38193d6da5..a714f1bd2c3 100644 --- a/src/typechecker/FStar.TypeChecker.Primops.Range.fst +++ b/src/typechecker/FStar.TypeChecker.Primops.Range.fst @@ -14,11 +14,43 @@ module Z = FStar.BigInt (* Range ops *) -let ops = [ - mk5 0 PC.mk_range_lid (fun fn from_l from_c to_l to_c -> - mk_range fn (mk_pos (Z.to_int_fs from_l) (Z.to_int_fs from_c)) - (mk_pos (Z.to_int_fs to_l) (Z.to_int_fs to_c)) - ); +(* this type only here to use typeclass hackery *) +type unsealedRange = | U of Range.range + +let mk_range (fn : string) (from_l from_c to_l to_c : Z.t) : Range.range = + Range.mk_range fn (mk_pos (Z.to_int_fs from_l) (Z.to_int_fs from_c)) + (mk_pos (Z.to_int_fs to_l) (Z.to_int_fs to_c)) + +let __mk_range (fn : string) (from_l from_c to_l to_c : Z.t) : unsealedRange = + U (mk_range fn from_l from_c to_l to_c) + +let explode (r : unsealedRange) : (string & Z.t & Z.t & Z.t & Z.t) = + match r with + | U r -> + let open FStar.Compiler.Range.Type in + (file_of_range r, + Z.of_int_fs (line_of_pos (start_of_range r)), + Z.of_int_fs (col_of_pos (start_of_range r)), + Z.of_int_fs (line_of_pos (end_of_range r)), + Z.of_int_fs (col_of_pos (end_of_range r))) +instance e_unsealedRange : Syntax.Embeddings.embedding unsealedRange = + let open FStar.Syntax.Embeddings in + embed_as e___range + (fun r -> U r) + (fun (U r) -> r) + None + +instance nbe_e_unsealedRange : FStar.TypeChecker.NBETerm.embedding unsealedRange = + let open FStar.TypeChecker.NBETerm in + embed_as e___range + (fun r -> U r) + (fun (U r) -> r) + None + +let ops = [ + mk5 0 PC.__mk_range_lid __mk_range; + mk5 0 PC.mk_range_lid mk_range; + mk1 0 PC.__explode_range_lid explode; mk2 0 PC.join_range_lid FStar.Compiler.Range.union_ranges; ] diff --git a/ulib/FStar.Range.fsti b/ulib/FStar.Range.fsti index c44506b68df..b8b8bdfda64 100644 --- a/ulib/FStar.Range.fsti +++ b/ulib/FStar.Range.fsti @@ -17,20 +17,37 @@ module FStar.Range open FStar.Sealed -(** [range] is a type for the internal representations of source - ranges The functions that follow below allow manipulating ranges - abstractly. Importantly, while we allow constructing ranges, we do - not allow destructing them, since that would reveal that - internally, set_range_of is not an identity function. *) +(** [__range] is a type for the internal representations of source + ranges. Internally, it includes a "definition" range and a "use" range, each + of which has a filename, a start position (line+col), and an end position. + + We do not fully expose this type, but explode below allows to inspect it, + and __mk_range to construct it. + + [range] is a sealed version of [__range], meaning it does not provide + any facts about its values. We use this type since we have *total* functions + inspecting terms and returning their range metadada (like the range_of constant). + Given that range is sealed, it is sound to make range_of total. +*) + assume new type __range type range = sealed __range (** A dummy range constant *) -val range_0 : range +val __range_0 : __range +let range_0 : range = seal __range_0 (** Building a range constant *) +val __mk_range (file: string) (from_line from_col to_line to_col: int) : Tot __range + val mk_range (file: string) (from_line from_col to_line to_col: int) : Tot range +(* This is essentially +unfold +let mk_range (file: string) (from_line from_col to_line to_col: int) : Tot range = + seal (__mk_range file from_line from_col to_line to_col) +but the extra indirection breaks the custom errors messages in QuickCode. +Just retaining this as a primop for now (Guido 30/Aug/2024) *) val join_range (r1 r2 : range) : Tot range @@ -38,3 +55,5 @@ val join_range (r1 r2 : range) : Tot range source-code location with an assertion. *) irreducible let labeled (r : range) (msg: string) (b: Type) : Type = b + +val explode (r : __range) : Tot (string * int * int * int * int)