From 1f105fc252839bdb61f281ff6037a7ac9dffada8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 21 Oct 2024 15:47:49 -0700 Subject: [PATCH 1/4] Syntax/Tc: Improving error range for expected failures When the set of errors do not match the expected set, we will highlight the @@expect_failure attribute instead of the whole definition. This works by adding a range to the Sig_fail sigelt, which is modifying the internal AST. However, since these Sig_fail signatures never make it to a .checked file, I don't think we need to bump the cache_version_number. --- src/FStarCompiler.fst.config.json | 2 +- src/extraction/FStarC.Extraction.ML.Modul.fst | 2 +- src/syntax/FStarC.Syntax.Syntax.fsti | 1 + src/syntax/FStarC.Syntax.VisitM.fst | 6 ++-- src/tosyntax/FStarC.ToSyntax.ToSyntax.fst | 32 +++++++++---------- src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti | 6 ++-- src/typechecker/FStarC.TypeChecker.Env.fst | 4 +-- src/typechecker/FStarC.TypeChecker.Tc.fst | 4 +-- 8 files changed, 29 insertions(+), 28 deletions(-) diff --git a/src/FStarCompiler.fst.config.json b/src/FStarCompiler.fst.config.json index e0e64dc3aa2..d59e9c396f6 100644 --- a/src/FStarCompiler.fst.config.json +++ b/src/FStarCompiler.fst.config.json @@ -1,5 +1,5 @@ { - "fstar_exe": "fstar.exe", + "fstar_exe": "../bin/fstar.exe", "options": [ "--MLish", "--MLish_effect", "FStarC.Compiler.Effect", diff --git a/src/extraction/FStarC.Extraction.ML.Modul.fst b/src/extraction/FStarC.Extraction.ML.Modul.fst index 3fb250f74bd..29ce94cc8ea 100644 --- a/src/extraction/FStarC.Extraction.ML.Modul.fst +++ b/src/extraction/FStarC.Extraction.ML.Modul.fst @@ -171,7 +171,7 @@ let rec extract_meta x : option meta = false x FStarC.Parser.Const.remove_unused_type_parameters_lid) with | None -> None - | Some l -> Some (RemoveUnusedTypeParameters (l, S.range_of_fv fv)) + | Some (l, _rng) -> Some (RemoveUnusedTypeParameters (l, S.range_of_fv fv)) end | _ -> None diff --git a/src/syntax/FStarC.Syntax.Syntax.fsti b/src/syntax/FStarC.Syntax.Syntax.fsti index 6677964d180..2ff1febe171 100644 --- a/src/syntax/FStarC.Syntax.Syntax.fsti +++ b/src/syntax/FStarC.Syntax.Syntax.fsti @@ -752,6 +752,7 @@ type sigelt' = } | Sig_fail { errs:list int; // Expected errors (empty for 'any') + rng: Range.range; // range of the `expect_failure`, for error reporting fail_in_lax:bool; // true if should fail in --lax ses:list sigelt; // The sigelts to be checked } diff --git a/src/syntax/FStarC.Syntax.VisitM.fst b/src/syntax/FStarC.Syntax.VisitM.fst index 1eadbd49fd0..ba608304061 100644 --- a/src/syntax/FStarC.Syntax.VisitM.fst +++ b/src/syntax/FStarC.Syntax.VisitM.fst @@ -457,9 +457,9 @@ let rec on_sub_sigelt' #m {|d : lvm m |} (se : sigelt') : m sigelt' = (* These two below are hardly used, since they disappear after typechecking, but are still useful so the desugarer can make use of deep_compress_se. *) - | Sig_fail {errs; fail_in_lax; ses} -> + | Sig_fail {rng; errs; fail_in_lax; ses} -> let! ses = ses |> mapM on_sub_sigelt in - return <| Sig_fail {errs; fail_in_lax; ses} + return <| Sig_fail {rng; errs; fail_in_lax; ses} | Sig_splice {is_typed; lids; tac} -> let! tac = tac |> f_term in @@ -537,4 +537,4 @@ in let lids, _ = Writer.run_writer m in BU.print1 "Lids = %s\n" (show lids); -*) \ No newline at end of file +*) diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst index df23e6017a6..080808ea591 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst @@ -644,8 +644,8 @@ let rec generalize_annotated_univs (s:sigelt) :sigelt = comp=Subst.subst_comp usubst c; cflags=flags} } - | Sig_fail {errs; fail_in_lax=lax; ses} -> - { s with sigel = Sig_fail {errs; + | Sig_fail {errs; rng; fail_in_lax=lax; ses} -> + { s with sigel = Sig_fail {errs; rng; fail_in_lax=lax; ses=List.map generalize_annotated_univs ses} } @@ -3260,7 +3260,7 @@ let push_reflect_effect env quals (effect_name:Ident.lid) range = Env.push_sigelt env refl_decl // FIXME: Add docs to refl_decl? else env -let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int) & bool = +let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int & Range.range) & bool = let warn () = if warn then Errors.log_issue at Errors.Warning_UnappliedFail @@ -3271,12 +3271,12 @@ let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int) & bo | Tm_fvar fv when S.fv_eq_lid fv head -> begin match args with - | [] -> Some [], true + | [] -> Some ([], at.pos), true | [(a1, _)] -> begin match EMB.unembed a1 EMB.id_norm_cb with | Some es -> - Some (List.map FStarC.BigInt.to_int_fs es), true + Some (List.map FStarC.BigInt.to_int_fs es, at.pos), true | _ -> warn(); None, true @@ -3291,11 +3291,11 @@ let parse_attr_with_list warn (at:S.term) (head:lident) : option (list int) & bo // If this is an expect_failure attribute, return the listed errors and whether it's a expect_lax_failure or not -let get_fail_attr1 warn (at : S.term) : option (list int & bool) = +let get_fail_attr1 warn (at : S.term) : option (list int & Range.range & bool) = let rebind res b = match res with | None -> None - | Some l -> Some (l, b) + | Some (l, rng) -> Some (l, rng, b) in let res, matched = parse_attr_with_list warn at C.fail_attr in if matched then rebind res false @@ -3303,15 +3303,15 @@ let get_fail_attr1 warn (at : S.term) : option (list int & bool) = rebind res true // Traverse a list of attributes to find all expect_failures and combine them -let get_fail_attr warn (ats : list S.term) : option (list int & bool) = +let get_fail_attr warn (ats : list S.term) : option (list int & Range.range & bool) = let comb f1 f2 = match f1, f2 with - | Some (e1, l1), Some (e2, l2) -> - Some (e1@e2, l1 || l2) + | Some (e1, rng1, l1), Some (e2, rng2, l2) -> + Some (e1@e2, rng1 `Range.union_ranges` rng2, l1 || l2) - | Some (e, l), None - | None, Some (e, l) -> - Some (e, l) + | Some x, None + | None, Some x -> + Some x | _ -> None in @@ -3652,7 +3652,7 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) = let attrs = List.map (desugar_term env) d.attrs in let attrs = U.deduplicate_terms attrs in match get_fail_attr false attrs with - | Some (expected_errs, lax) -> + | Some (expected_errs, err_rng, lax) -> // The `fail` attribute behaves // differentrly! We only keep that one on the first new decl. let env0 = @@ -3668,7 +3668,7 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) = (* Succeeded desugaring, carry on, but make a Sig_fail *) (* Restore attributes, except for fail *) let ses = List.map (fun se -> { se with sigattrs = no_fail_attrs attrs }) ses in - let se = { sigel = Sig_fail {errs=expected_errs; fail_in_lax=lax; ses}; + let se = { sigel = Sig_fail {rng=err_rng;errs=expected_errs; fail_in_lax=lax; ses}; sigquals = []; sigrng = d.drange; sigmeta = default_sigmeta; @@ -3695,7 +3695,7 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) = let open FStarC.Class.PP in let open FStarC.Pprint in List.iter Errors.print_issue errs; - Errors.log_issue d Errors.Error_DidNotFail [ + Errors.log_issue err_rng Errors.Error_DidNotFail [ prefix 2 1 (text "This top-level definition was expected to raise error codes") (pp expected_errs) ^/^ diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti index 8c153e658cb..7bb8b17cad1 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti @@ -54,7 +54,7 @@ val add_modul_to_env: Syntax.modul -> erase_univs:(S.term -> S.term) -> withenv unit -val parse_attr_with_list : bool -> S.term -> lident -> option (list int) & bool +val parse_attr_with_list : bool -> S.term -> lident -> option (list int & Range.range) & bool -val get_fail_attr1 : bool -> S.term -> option (list int & bool) -val get_fail_attr : bool -> list S.term -> option (list int & bool) +val get_fail_attr1 : bool -> S.term -> option (list int & Range.range & bool) +val get_fail_attr : bool -> list S.term -> option (list int & Range.range & bool) diff --git a/src/typechecker/FStarC.TypeChecker.Env.fst b/src/typechecker/FStarC.TypeChecker.Env.fst index a8ebf4d6dd9..e6c9206ac78 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fst +++ b/src/typechecker/FStarC.TypeChecker.Env.fst @@ -943,7 +943,7 @@ let fv_has_erasable_attr env fv = cache_in_fv_tab env.erasable_types_tab fv f let fv_has_strict_args env fv = - let f () = + let f () : bool & option (list int) = let attrs = lookup_attrs_of_lid env (S.lid_of_fv fv) in match attrs with | None -> false, None @@ -953,7 +953,7 @@ let fv_has_strict_args env fv = fst (FStarC.ToSyntax.ToSyntax.parse_attr_with_list false x FStarC.Parser.Const.strict_on_arguments_attr)) in - true, res + true, BU.map_opt res fst in cache_in_fv_tab env.strict_args_tab fv f diff --git a/src/typechecker/FStarC.TypeChecker.Tc.fst b/src/typechecker/FStarC.TypeChecker.Tc.fst index fb673b295bf..4ccd7d83b7d 100644 --- a/src/typechecker/FStarC.TypeChecker.Tc.fst +++ b/src/typechecker/FStarC.TypeChecker.Tc.fst @@ -584,7 +584,7 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env = (Print.sigelt_to_string_short se); [], [], env - | Sig_fail {errs=expected_errors; fail_in_lax=lax; ses} -> + | Sig_fail {rng=fail_rng; errs=expected_errors; fail_in_lax=lax; ses} -> let env' = if lax then { env with admit = true } else env in let env' = Env.push env' "expect_failure" in (* We need to call push since tc_decls will encode the sigelts that @@ -626,7 +626,7 @@ let tc_decl' env0 se: list sigelt & list sigelt & Env.env = let open FStarC.Pprint in let open FStarC.Errors.Msg in List.iter Errors.print_issue errs; - Errors.log_issue se Errors.Error_DidNotFail [ + Errors.log_issue fail_rng Errors.Error_DidNotFail [ prefix 2 1 (text "This top-level definition was expected to raise error codes") (pp expected_errors) ^/^ From 8aa6ca5122b806b92a404ef94e742c7207e51d3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 22 Oct 2024 17:21:36 -0700 Subject: [PATCH 2/4] Tc: improve some errors --- src/typechecker/FStarC.TypeChecker.TcTerm.fst | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.TcTerm.fst b/src/typechecker/FStarC.TypeChecker.TcTerm.fst index a2bbd9f07c8..28e7720dec6 100644 --- a/src/typechecker/FStarC.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStarC.TypeChecker.TcTerm.fst @@ -4195,11 +4195,14 @@ and build_let_rec_env _top_level env lbs : list letbinding & env_t & guard_t = // TODO: There's a similar error in check_let_recs, would be nice // to remove this one. if List.isEmpty formals || List.isEmpty actuals then - raise_error lbtyp Errors.Fatal_RecursiveFunctionLiteral // TODO: GM: maybe point to the one that's actually empty? - (BU.format3 "Only function literals with arrow types can be defined recursively; got (%s) %s : %s" + // TODO: GM: maybe point to the one that's actually empty? + raise_error lbtyp Errors.Fatal_RecursiveFunctionLiteral [ + text "Only function literals with arrow types can be defined recursively."; + text <| (BU.format3 "Got (%s) %s : %s" (tag_of lbdef) (show lbdef) (show lbtyp)); + ]; let nformals = List.length formals in @@ -4266,12 +4269,13 @@ and check_let_recs env lbts = let bs, t, lcomp = abs_formals lb.lbdef in //see issue #1017 match bs with - | [] -> raise_error (S.range_of_lbname lb.lbname) - Errors.Fatal_RecursiveFunctionLiteral - (BU.format2 - "Only function literals may be defined recursively; %s is defined to be %s" + | [] -> + raise_error (S.range_of_lbname lb.lbname) Errors.Fatal_RecursiveFunctionLiteral [ + text "Only function literals may be defined recursively."; + text <| (BU.format2 "%s is defined to be %s" (show lb.lbname) - (show lb.lbdef)) + (show lb.lbdef)); + ] | _ -> (); (* HACK ALERT: arity From 221cacf4d73d5666e39993cd3a9d0b07a0c49a9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 22 Oct 2024 14:48:59 -0700 Subject: [PATCH 3/4] nit in error message --- src/syntax/FStarC.Syntax.Util.fst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/syntax/FStarC.Syntax.Util.fst b/src/syntax/FStarC.Syntax.Util.fst index bd7dc1d2627..cb30ec79834 100644 --- a/src/syntax/FStarC.Syntax.Util.fst +++ b/src/syntax/FStarC.Syntax.Util.fst @@ -1810,8 +1810,8 @@ let destruct_lemma_with_smt_patterns (t:term) Errors.raise_error p Errors.Error_IllSMTPat [ prefix 2 1 (text "Not an atomic SMT pattern:") (ttd p); - text "Patterns on lemmas must be a list of simple SMTPat's;\ - or a single SMTPatOr containing a list;\ + text "Patterns on lemmas must be a list of simple SMTPat's; \ + or a single SMTPatOr containing a list \ of lists of patterns." ] in 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 4/4] 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 =