From 7392d959f885c2d4809e00b679b27d94b7c4278c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 22 Oct 2024 17:27:40 -0700 Subject: [PATCH] snap --- .../generated/FStarC_Extraction_ML_Modul.ml | 2 +- .../generated/FStarC_Syntax_Print.ml | 11 ++-- .../generated/FStarC_Syntax_Print_Ugly.ml | 14 +++-- .../generated/FStarC_Syntax_Syntax.ml | 21 +++++-- .../fstar-lib/generated/FStarC_Syntax_Util.ml | 2 +- .../generated/FStarC_Syntax_VisitM.ml | 2 + .../generated/FStarC_ToSyntax_ToSyntax.ml | 50 +++++++++------ .../generated/FStarC_TypeChecker_Env.ml | 4 +- .../generated/FStarC_TypeChecker_Tc.ml | 16 ++--- .../generated/FStarC_TypeChecker_TcTerm.ml | 63 ++++++++++++------- 10 files changed, 117 insertions(+), 68 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStarC_Extraction_ML_Modul.ml index 80b1942419c..2db1c39678c 100644 --- a/ocaml/fstar-lib/generated/FStarC_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStarC_Extraction_ML_Modul.ml @@ -326,7 +326,7 @@ let rec (extract_meta : (match uu___5 with | FStar_Pervasives_Native.None -> FStar_Pervasives_Native.None - | FStar_Pervasives_Native.Some l -> + | FStar_Pervasives_Native.Some (l, _rng) -> let uu___6 = let uu___7 = let uu___8 = FStarC_Syntax_Syntax.range_of_fv fv in diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml index c8c141e0e71..c2cdcf8c141 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml @@ -778,13 +778,14 @@ let rec (sigelt_to_string_short : sigelt_to_string_short uu___1 | FStarC_Syntax_Syntax.Sig_fail { FStarC_Syntax_Syntax.errs = uu___; - FStarC_Syntax_Syntax.fail_in_lax = uu___1; + FStarC_Syntax_Syntax.rng1 = uu___1; + FStarC_Syntax_Syntax.fail_in_lax = uu___2; FStarC_Syntax_Syntax.ses1 = ses;_} -> - let uu___2 = - let uu___3 = FStarC_Compiler_List.hd ses in - sigelt_to_string_short uu___3 in - FStarC_Compiler_Util.format1 "[@@expect_failure] %s" uu___2 + let uu___3 = + let uu___4 = FStarC_Compiler_List.hd ses in + sigelt_to_string_short uu___4 in + FStarC_Compiler_Util.format1 "[@@expect_failure] %s" uu___3 | FStarC_Syntax_Syntax.Sig_new_effect ed -> let kw = let uu___ = FStarC_Syntax_Util.is_layered ed in diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Print_Ugly.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Print_Ugly.ml index 749e227a807..dd5682ccb86 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Print_Ugly.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Print_Ugly.ml @@ -1354,18 +1354,20 @@ let rec (sigelt_to_string : FStarC_Syntax_Syntax.sigelt -> Prims.string) = Prims.strcat "(* Sig_bundle *)" uu___1 | FStarC_Syntax_Syntax.Sig_fail { FStarC_Syntax_Syntax.errs = errs; + FStarC_Syntax_Syntax.rng1 = uu___; FStarC_Syntax_Syntax.fail_in_lax = lax; FStarC_Syntax_Syntax.ses1 = ses;_} -> - let uu___ = FStarC_Compiler_Util.string_of_bool lax in - let uu___1 = + let uu___1 = FStarC_Compiler_Util.string_of_bool lax in + let uu___2 = (FStarC_Common.string_of_list ()) FStarC_Compiler_Util.string_of_int errs in - let uu___2 = - let uu___3 = FStarC_Compiler_List.map sigelt_to_string ses in - FStarC_Compiler_String.concat "\n" uu___3 in + let uu___3 = + let uu___4 = FStarC_Compiler_List.map sigelt_to_string ses in + FStarC_Compiler_String.concat "\n" uu___4 in FStarC_Compiler_Util.format3 - "(* Sig_fail %s %s *)\n%s\n(* / Sig_fail*)\n" uu___ uu___1 uu___2 + "(* Sig_fail %s %s *)\n%s\n(* / Sig_fail*)\n" uu___1 uu___2 + uu___3 | FStarC_Syntax_Syntax.Sig_new_effect ed -> let uu___ = let uu___1 = FStarC_Syntax_Util.is_dm4f ed in diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml index dbc45fd882b..9c8fa55e710 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Syntax.ml @@ -2053,6 +2053,7 @@ and sigelt'__Sig_polymonadic_subcomp__payload = and sigelt'__Sig_fail__payload = { errs: Prims.int Prims.list ; + rng1: FStarC_Compiler_Range_Type.range ; fail_in_lax: Prims.bool ; ses1: sigelt Prims.list } and sigelt' = @@ -2323,15 +2324,23 @@ let (__proj__Mksigelt'__Sig_polymonadic_subcomp__payload__item__kind : let (__proj__Mksigelt'__Sig_fail__payload__item__errs : sigelt'__Sig_fail__payload -> Prims.int Prims.list) = fun projectee -> - match projectee with | { errs; fail_in_lax; ses1 = ses;_} -> errs + match projectee with + | { errs; rng1 = rng; fail_in_lax; ses1 = ses;_} -> errs +let (__proj__Mksigelt'__Sig_fail__payload__item__rng : + sigelt'__Sig_fail__payload -> FStarC_Compiler_Range_Type.range) = + fun projectee -> + match projectee with + | { errs; rng1 = rng; fail_in_lax; ses1 = ses;_} -> rng let (__proj__Mksigelt'__Sig_fail__payload__item__fail_in_lax : sigelt'__Sig_fail__payload -> Prims.bool) = fun projectee -> - match projectee with | { errs; fail_in_lax; ses1 = ses;_} -> fail_in_lax + match projectee with + | { errs; rng1 = rng; fail_in_lax; ses1 = ses;_} -> fail_in_lax let (__proj__Mksigelt'__Sig_fail__payload__item__ses : sigelt'__Sig_fail__payload -> sigelt Prims.list) = fun projectee -> - match projectee with | { errs; fail_in_lax; ses1 = ses;_} -> ses + match projectee with + | { errs; rng1 = rng; fail_in_lax; ses1 = ses;_} -> ses let (uu___is_Sig_inductive_typ : sigelt' -> Prims.bool) = fun projectee -> match projectee with | Sig_inductive_typ _0 -> true | uu___ -> false @@ -3455,6 +3464,8 @@ let (tagged_sigelt : sigelt FStarC_Class_Tagged.tagged) = { m_lid1 = uu___; n_lid1 = uu___1; tm4 = uu___2; typ1 = uu___3; kind2 = uu___4;_} -> "Sig_polymonadic_subcomp" - | Sig_fail { errs = uu___; fail_in_lax = uu___1; ses1 = uu___2;_} -> - "Sig_fail") + | Sig_fail + { errs = uu___; rng1 = uu___1; fail_in_lax = uu___2; + ses1 = uu___3;_} + -> "Sig_fail") } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml index 50679025adf..a01755610f4 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml @@ -4074,7 +4074,7 @@ let (destruct_lemma_with_smt_patterns : let uu___5 = let uu___6 = FStarC_Errors_Msg.text - "Patterns on lemmas must be a list of simple SMTPat's;or a single SMTPatOr containing a list;of lists of patterns." in + "Patterns on lemmas must be a list of simple SMTPat's; or a single SMTPatOr containing a list of lists of patterns." in [uu___6] in uu___4 :: uu___5 in FStarC_Errors.raise_error diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_VisitM.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_VisitM.ml index e59adad2db4..549d80b24f9 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_VisitM.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_VisitM.ml @@ -2080,6 +2080,7 @@ let rec on_sub_sigelt' : 'm . 'm lvm -> FStarC_Syntax_Syntax.sigelt' -> 'm = })))) uu___2))) uu___1) | FStarC_Syntax_Syntax.Sig_fail { FStarC_Syntax_Syntax.errs = errs; + FStarC_Syntax_Syntax.rng1 = rng; FStarC_Syntax_Syntax.fail_in_lax = fail_in_lax; FStarC_Syntax_Syntax.ses1 = ses;_} -> @@ -2097,6 +2098,7 @@ let rec on_sub_sigelt' : 'm . 'm lvm -> FStarC_Syntax_Syntax.sigelt' -> 'm = (FStarC_Syntax_Syntax.Sig_fail { FStarC_Syntax_Syntax.errs = errs; + FStarC_Syntax_Syntax.rng1 = rng; FStarC_Syntax_Syntax.fail_in_lax = fail_in_lax; FStarC_Syntax_Syntax.ses1 = ses1 })))) uu___1) diff --git a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml index 977fd593e8f..41157d34b1c 100644 --- a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml @@ -1326,7 +1326,7 @@ let rec (generalize_annotated_univs : FStarC_Syntax_Syntax.sigopts = (s.FStarC_Syntax_Syntax.sigopts) } | FStarC_Syntax_Syntax.Sig_fail - { FStarC_Syntax_Syntax.errs = errs; + { FStarC_Syntax_Syntax.errs = errs; FStarC_Syntax_Syntax.rng1 = rng; FStarC_Syntax_Syntax.fail_in_lax = lax; FStarC_Syntax_Syntax.ses1 = ses;_} -> @@ -1336,6 +1336,7 @@ let rec (generalize_annotated_univs : FStarC_Compiler_List.map generalize_annotated_univs ses in { FStarC_Syntax_Syntax.errs = errs; + FStarC_Syntax_Syntax.rng1 = rng; FStarC_Syntax_Syntax.fail_in_lax = lax; FStarC_Syntax_Syntax.ses1 = uu___3 } in @@ -8138,7 +8139,8 @@ let (parse_attr_with_list : Prims.bool -> FStarC_Syntax_Syntax.term -> FStarC_Ident.lident -> - (Prims.int Prims.list FStar_Pervasives_Native.option * Prims.bool)) + ((Prims.int Prims.list * FStarC_Compiler_Range_Type.range) + FStar_Pervasives_Native.option * Prims.bool)) = fun warn -> fun at -> @@ -8167,7 +8169,9 @@ let (parse_attr_with_list : | FStarC_Syntax_Syntax.Tm_fvar fv when FStarC_Syntax_Syntax.fv_eq_lid fv head -> (match args with - | [] -> ((FStar_Pervasives_Native.Some []), true) + | [] -> + ((FStar_Pervasives_Native.Some + ([], (at.FStarC_Syntax_Syntax.pos))), true) | (a1, uu___2)::[] -> let uu___3 = FStarC_Syntax_Embeddings_Base.unembed @@ -8178,8 +8182,10 @@ let (parse_attr_with_list : | FStar_Pervasives_Native.Some es -> let uu___4 = let uu___5 = - FStarC_Compiler_List.map - FStarC_BigInt.to_int_fs es in + let uu___6 = + FStarC_Compiler_List.map + FStarC_BigInt.to_int_fs es in + (uu___6, (at.FStarC_Syntax_Syntax.pos)) in FStar_Pervasives_Native.Some uu___5 in (uu___4, true) | uu___4 -> @@ -8190,15 +8196,16 @@ let (parse_attr_with_list : let (get_fail_attr1 : Prims.bool -> FStarC_Syntax_Syntax.term -> - (Prims.int Prims.list * Prims.bool) FStar_Pervasives_Native.option) + (Prims.int Prims.list * FStarC_Compiler_Range_Type.range * Prims.bool) + FStar_Pervasives_Native.option) = fun warn -> fun at -> let rebind res b = match res with | FStar_Pervasives_Native.None -> FStar_Pervasives_Native.None - | FStar_Pervasives_Native.Some l -> - FStar_Pervasives_Native.Some (l, b) in + | FStar_Pervasives_Native.Some (l, rng) -> + FStar_Pervasives_Native.Some (l, rng, b) in let uu___ = parse_attr_with_list warn at FStarC_Parser_Const.fail_attr in match uu___ with | (res, matched) -> @@ -8211,20 +8218,23 @@ let (get_fail_attr1 : let (get_fail_attr : Prims.bool -> FStarC_Syntax_Syntax.term Prims.list -> - (Prims.int Prims.list * Prims.bool) FStar_Pervasives_Native.option) + (Prims.int Prims.list * FStarC_Compiler_Range_Type.range * Prims.bool) + FStar_Pervasives_Native.option) = fun warn -> fun ats -> let comb f1 f2 = match (f1, f2) with - | (FStar_Pervasives_Native.Some (e1, l1), - FStar_Pervasives_Native.Some (e2, l2)) -> - FStar_Pervasives_Native.Some - ((FStarC_Compiler_List.op_At e1 e2), (l1 || l2)) - | (FStar_Pervasives_Native.Some (e, l), FStar_Pervasives_Native.None) - -> FStar_Pervasives_Native.Some (e, l) - | (FStar_Pervasives_Native.None, FStar_Pervasives_Native.Some (e, l)) - -> FStar_Pervasives_Native.Some (e, l) + | (FStar_Pervasives_Native.Some (e1, rng1, l1), + FStar_Pervasives_Native.Some (e2, rng2, l2)) -> + let uu___ = + let uu___1 = FStarC_Compiler_Range_Ops.union_ranges rng1 rng2 in + ((FStarC_Compiler_List.op_At e1 e2), uu___1, (l1 || l2)) in + FStar_Pervasives_Native.Some uu___ + | (FStar_Pervasives_Native.Some x, FStar_Pervasives_Native.None) -> + FStar_Pervasives_Native.Some x + | (FStar_Pervasives_Native.None, FStar_Pervasives_Native.Some x) -> + FStar_Pervasives_Native.Some x | uu___ -> FStar_Pervasives_Native.None in FStarC_Compiler_List.fold_right (fun at -> @@ -9184,7 +9194,7 @@ and (desugar_decl_maybe_fail_attr : let attrs1 = FStarC_Syntax_Util.deduplicate_terms attrs in let uu___1 = get_fail_attr false attrs1 in match uu___1 with - | FStar_Pervasives_Native.Some (expected_errs, lax) -> + | FStar_Pervasives_Native.Some (expected_errs, err_rng, lax) -> let env0 = let uu___2 = FStarC_Syntax_DsEnv.snapshot env in FStar_Pervasives_Native.snd uu___2 in @@ -9233,6 +9243,7 @@ and (desugar_decl_maybe_fail_attr : (FStarC_Syntax_Syntax.Sig_fail { FStarC_Syntax_Syntax.errs = expected_errs; + FStarC_Syntax_Syntax.rng1 = err_rng; FStarC_Syntax_Syntax.fail_in_lax = lax; FStarC_Syntax_Syntax.ses1 = ses1 }); @@ -9328,7 +9339,8 @@ and (desugar_decl_maybe_fail_attr : [uu___11] in uu___9 :: uu___10 in FStarC_Errors.log_issue - FStarC_Parser_AST.hasRange_decl d1 + FStarC_Class_HasRange.hasRange_range + err_rng FStarC_Errors_Codes.Error_DidNotFail () (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml index f8d34157341..1f71e05cc5e 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml @@ -4143,7 +4143,9 @@ let (fv_has_strict_args : FStarC_ToSyntax_ToSyntax.parse_attr_with_list false x FStarC_Parser_Const.strict_on_arguments_attr in FStar_Pervasives_Native.fst uu___1) in - (true, res) in + let uu___1 = + FStarC_Compiler_Util.map_opt res FStar_Pervasives_Native.fst in + (true, uu___1) in cache_in_fv_tab env1.strict_args_tab fv f let (try_lookup_effect_lid : env -> diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml index 1fa9c884454..06202fc9609 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml @@ -2108,21 +2108,23 @@ let (tc_decl' : failwith "Impossible bare data-constructor" | FStarC_Syntax_Syntax.Sig_fail { FStarC_Syntax_Syntax.errs = uu___2; + FStarC_Syntax_Syntax.rng1 = uu___3; FStarC_Syntax_Syntax.fail_in_lax = false; - FStarC_Syntax_Syntax.ses1 = uu___3;_} + FStarC_Syntax_Syntax.ses1 = uu___4;_} when env.FStarC_TypeChecker_Env.admit -> - ((let uu___5 = FStarC_Compiler_Debug.any () in - if uu___5 + ((let uu___6 = FStarC_Compiler_Debug.any () in + if uu___6 then - let uu___6 = + let uu___7 = FStarC_Syntax_Print.sigelt_to_string_short se2 in FStarC_Compiler_Util.print1 "Skipping %s since env.admit=true and this is not an expect_lax_failure\n" - uu___6 + uu___7 else ()); ([], [], env)) | FStarC_Syntax_Syntax.Sig_fail { FStarC_Syntax_Syntax.errs = expected_errors; + FStarC_Syntax_Syntax.rng1 = fail_rng; FStarC_Syntax_Syntax.fail_in_lax = lax; FStarC_Syntax_Syntax.ses1 = ses;_} -> @@ -2357,8 +2359,8 @@ let (tc_decl' : [uu___14] in uu___12 :: uu___13 in FStarC_Errors.log_issue - FStarC_Syntax_Syntax.has_range_sigelt - se2 + FStarC_Class_HasRange.hasRange_range + fail_rng FStarC_Errors_Codes.Error_DidNotFail () (Obj.magic diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml index 76a97476ce6..3bf3577a273 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml @@ -11715,23 +11715,32 @@ and (build_let_rec_env : then (let uu___5 = let uu___6 = - FStarC_Class_Tagged.tag_of - FStarC_Syntax_Syntax.tagged_term lbdef in + FStarC_Errors_Msg.text + "Only function literals with arrow types can be defined recursively." in let uu___7 = - FStarC_Class_Show.show - FStarC_Syntax_Print.showable_term lbdef in - let uu___8 = - FStarC_Class_Show.show - FStarC_Syntax_Print.showable_term lbtyp in - FStarC_Compiler_Util.format3 - "Only function literals with arrow types can be defined recursively; got (%s) %s : %s" - uu___6 uu___7 uu___8 in + let uu___8 = + let uu___9 = + let uu___10 = + FStarC_Class_Tagged.tag_of + FStarC_Syntax_Syntax.tagged_term lbdef in + let uu___11 = + FStarC_Class_Show.show + FStarC_Syntax_Print.showable_term lbdef in + let uu___12 = + FStarC_Class_Show.show + FStarC_Syntax_Print.showable_term lbtyp in + FStarC_Compiler_Util.format3 + "Got (%s) %s : %s" uu___10 uu___11 + uu___12 in + FStarC_Errors_Msg.text uu___9 in + [uu___8] in + uu___6 :: uu___7 in FStarC_Errors.raise_error (FStarC_Syntax_Syntax.has_range_syntax ()) lbtyp FStarC_Errors_Codes.Fatal_RecursiveFunctionLiteral () (Obj.magic - FStarC_Errors_Msg.is_error_message_string) + FStarC_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___5)) else (); (let nformals = FStarC_Compiler_List.length formals in @@ -12146,24 +12155,32 @@ and (check_let_recs : lb.FStarC_Syntax_Syntax.lbname in let uu___4 = let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.show_either - FStarC_Syntax_Print.showable_bv - FStarC_Syntax_Print.showable_fv) - lb.FStarC_Syntax_Syntax.lbname in + FStarC_Errors_Msg.text + "Only function literals may be defined recursively." in let uu___6 = - FStarC_Class_Show.show - FStarC_Syntax_Print.showable_term - lb.FStarC_Syntax_Syntax.lbdef in - FStarC_Compiler_Util.format2 - "Only function literals may be defined recursively; %s is defined to be %s" - uu___5 uu___6 in + let uu___7 = + let uu___8 = + let uu___9 = + FStarC_Class_Show.show + (FStarC_Class_Show.show_either + FStarC_Syntax_Print.showable_bv + FStarC_Syntax_Print.showable_fv) + lb.FStarC_Syntax_Syntax.lbname in + let uu___10 = + FStarC_Class_Show.show + FStarC_Syntax_Print.showable_term + lb.FStarC_Syntax_Syntax.lbdef in + FStarC_Compiler_Util.format2 + "%s is defined to be %s" uu___9 uu___10 in + FStarC_Errors_Msg.text uu___8 in + [uu___7] in + uu___5 :: uu___6 in FStarC_Errors.raise_error FStarC_Class_HasRange.hasRange_range uu___3 FStarC_Errors_Codes.Fatal_RecursiveFunctionLiteral () (Obj.magic - FStarC_Errors_Msg.is_error_message_string) + FStarC_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___4) | uu___3 -> let arity =