From 8be572151d59e6ddb9ffa452f4774c25aa89c7da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 10 Aug 2023 10:06:37 -0700 Subject: [PATCH 1/3] ToSyntax: improve some ranges With this change, the def-range for an inductive type or data constructor points to the source location where the name appears in the definition, and not the full recursive block. This means that hitting F12 in the VSCode extension over a type or constructor will be more precise. cc @nikswamy --- src/tosyntax/FStar.ToSyntax.ToSyntax.fst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index 30675e9e5b6..1f5fe7f80b6 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst @@ -2865,8 +2865,8 @@ let rec desugar_tycon env (d: AST.decl) (d_attrs:list S.term) quals tcs : (env_t concat_options additional_records @ [TyconVariant (id, bds, k, variants)] | tycon -> [tycon] in let tcs = concatMap desugar_tycon_variant_record tcs in - let tot = mk_term (Name (C.effect_Tot_lid)) rng Expr in - let with_constructor_effect t = mk_term (App(tot, t, Nothing)) t.range t.level in + let tot rng = mk_term (Name (C.effect_Tot_lid)) rng Expr in + let with_constructor_effect t = mk_term (App(tot t.range, t, Nothing)) t.range t.level in let apply_binders t binders = let imp_of_aqual (b:AST.binder) = match b.aqual with | Some Implicit @@ -2910,7 +2910,7 @@ let rec desugar_tycon env (d: AST.decl) (d_attrs:list S.term) quals tcs : (env_t mutuals; ds=[]}; sigquals = quals; - sigrng = rng; + sigrng = range_of_id id; sigmeta = default_sigmeta; sigattrs = d_attrs; sigopts = None } in @@ -2992,12 +2992,12 @@ let rec desugar_tycon env (d: AST.decl) (d_attrs:list S.term) quals tcs : (env_t { sigel = Sig_effect_abbrev {lid=qlid; us=[]; bs=typars; comp=c; cflags=cattributes @ comp_flags c}; sigquals = quals; - sigrng = rng; + sigrng = range_of_id id; sigmeta = default_sigmeta ; sigattrs = []; sigopts = None; } else let t = desugar_typ env' t in - mk_typ_abbrev env d qlid [] typars kopt t [qlid] quals rng in + mk_typ_abbrev env d qlid [] typars kopt t [qlid] quals (range_of_id id) in let env = push_sigelt env se in env, [se] @@ -3038,7 +3038,7 @@ let rec desugar_tycon env (d: AST.decl) (d_attrs:list S.term) quals tcs : (env_t let tpars = Subst.close_binders tpars in Subst.close tpars t in - [([], mk_typ_abbrev env d id uvs tpars (Some k) t [id] quals rng)] + [([], mk_typ_abbrev env d id uvs tpars (Some k) t [id] quals (range_of_lid id))] | Inl ({ sigel = Sig_inductive_typ {lid=tname; us=univs; @@ -3076,7 +3076,7 @@ let rec desugar_tycon env (d: AST.decl) (d_attrs:list S.term) quals tcs : (env_t num_ty_params=ntps; mutuals}; sigquals = quals; - sigrng = rng; + sigrng = range_of_lid name; sigmeta = default_sigmeta ; sigattrs = U.deduplicate_terms (val_attrs @ d_attrs @ map (desugar_term env) cons_attrs); sigopts = None; })))) @@ -3096,7 +3096,7 @@ let rec desugar_tycon env (d: AST.decl) (d_attrs:list S.term) quals tcs : (env_t mutuals; ds=constrNames}; sigquals = tname_quals; - sigrng = rng; + sigrng = range_of_lid tname; sigmeta = default_sigmeta ; sigattrs = U.deduplicate_terms (val_attrs @ d_attrs); sigopts = None; })::constrs From 4f870e4df5c2c560701377bf343330662745c535 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 10 Aug 2023 10:08:40 -0700 Subject: [PATCH 2/3] snap --- .../generated/FStar_ToSyntax_ToSyntax.ml | 55 ++++++++++++------- 1 file changed, 35 insertions(+), 20 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index 94f709ed519..a11e9b71454 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -6594,14 +6594,18 @@ let rec (desugar_tycon : | tycon -> [tycon] in let tcs1 = FStar_Compiler_List.concatMap desugar_tycon_variant_record tcs in - let tot = + let tot rng1 = FStar_Parser_AST.mk_term - (FStar_Parser_AST.Name FStar_Parser_Const.effect_Tot_lid) rng - FStar_Parser_AST.Expr in + (FStar_Parser_AST.Name FStar_Parser_Const.effect_Tot_lid) + rng1 FStar_Parser_AST.Expr in let with_constructor_effect t = - FStar_Parser_AST.mk_term - (FStar_Parser_AST.App (tot, t, FStar_Parser_AST.Nothing)) - t.FStar_Parser_AST.range t.FStar_Parser_AST.level in + let uu___ = + let uu___1 = + let uu___2 = tot t.FStar_Parser_AST.range in + (uu___2, t, FStar_Parser_AST.Nothing) in + FStar_Parser_AST.App uu___1 in + FStar_Parser_AST.mk_term uu___ t.FStar_Parser_AST.range + t.FStar_Parser_AST.level in let apply_binders t binders = let imp_of_aqual b = match b.FStar_Parser_AST.aqual with @@ -6722,6 +6726,7 @@ let rec (desugar_tycon : let typars1 = FStar_Syntax_Subst.close_binders typars in let k1 = FStar_Syntax_Subst.close typars1 k in let se = + let uu___2 = FStar_Ident.range_of_id id in { FStar_Syntax_Syntax.sigel = (FStar_Syntax_Syntax.Sig_inductive_typ @@ -6735,7 +6740,7 @@ let rec (desugar_tycon : FStar_Syntax_Syntax.mutuals = mutuals; FStar_Syntax_Syntax.ds = [] }); - FStar_Syntax_Syntax.sigrng = rng; + FStar_Syntax_Syntax.sigrng = uu___2; FStar_Syntax_Syntax.sigquals = quals1; FStar_Syntax_Syntax.sigmeta = FStar_Syntax_Syntax.default_sigmeta; @@ -6956,6 +6961,7 @@ let rec (desugar_tycon : match uu___3 with | FStar_Syntax_Syntax.Effect -> false | uu___4 -> true)) in + let uu___3 = FStar_Ident.range_of_id id in { FStar_Syntax_Syntax.sigel = (FStar_Syntax_Syntax.Sig_effect_abbrev @@ -6969,7 +6975,7 @@ let rec (desugar_tycon : cattributes (FStar_Syntax_Util.comp_flags c1)) }); - FStar_Syntax_Syntax.sigrng = rng; + FStar_Syntax_Syntax.sigrng = uu___3; FStar_Syntax_Syntax.sigquals = quals2; FStar_Syntax_Syntax.sigmeta = FStar_Syntax_Syntax.default_sigmeta; @@ -6979,8 +6985,9 @@ let rec (desugar_tycon : } else (let t1 = desugar_typ env' t in + let uu___3 = FStar_Ident.range_of_id id in mk_typ_abbrev env d qlid [] typars kopt1 t1 - [qlid] quals1 rng) in + [qlid] quals1 uu___3) in let env1 = FStar_Syntax_DsEnv.push_sigelt env se in (env1, [se])) | (FStar_Parser_AST.TyconRecord uu___)::[] -> @@ -7104,9 +7111,11 @@ let rec (desugar_tycon : t2) in let uu___12 = let uu___13 = + let uu___14 = + FStar_Ident.range_of_lid id in mk_typ_abbrev env1 d id uvs tpars (FStar_Pervasives_Native.Some k) t1 - [id] quals1 rng in + [id] quals1 uu___14 in ([], uu___13) in [uu___12] | FStar_Pervasives.Inl @@ -7279,9 +7288,12 @@ let rec (desugar_tycon : FStar_Syntax_Syntax.Sig_datacon uu___16 in let uu___16 = - let uu___17 = - let uu___18 = - let uu___19 + FStar_Ident.range_of_lid + name in + let uu___17 = + let uu___18 = + let uu___19 = + let uu___20 = FStar_Compiler_List.map (desugar_term @@ -7289,24 +7301,24 @@ let rec (desugar_tycon : cons_attrs in FStar_Compiler_List.op_At d_attrs - uu___19 in + uu___20 in FStar_Compiler_List.op_At val_attrs - uu___18 in + uu___19 in FStar_Syntax_Util.deduplicate_terms - uu___17 in + uu___18 in { FStar_Syntax_Syntax.sigel = uu___15; FStar_Syntax_Syntax.sigrng - = rng; + = uu___16; FStar_Syntax_Syntax.sigquals = quals2; FStar_Syntax_Syntax.sigmeta = FStar_Syntax_Syntax.default_sigmeta; FStar_Syntax_Syntax.sigattrs - = uu___16; + = uu___17; FStar_Syntax_Syntax.sigopts = FStar_Pervasives_Native.None @@ -7347,6 +7359,9 @@ let rec (desugar_tycon : (let uu___12 = let uu___13 = let uu___14 = + FStar_Ident.range_of_lid + tname in + let uu___15 = FStar_Syntax_Util.deduplicate_terms (FStar_Compiler_List.op_At val_attrs d_attrs) in @@ -7371,14 +7386,14 @@ let rec (desugar_tycon : = constrNames }); FStar_Syntax_Syntax.sigrng - = rng; + = uu___14; FStar_Syntax_Syntax.sigquals = tname_quals; FStar_Syntax_Syntax.sigmeta = FStar_Syntax_Syntax.default_sigmeta; FStar_Syntax_Syntax.sigattrs - = uu___14; + = uu___15; FStar_Syntax_Syntax.sigopts = FStar_Pervasives_Native.None From 36268777b8eec8472864a46f9e36f041e8fbc18e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 10 Aug 2023 10:48:23 -0700 Subject: [PATCH 3/3] error-messages: update, errors now point to type names --- tests/error-messages/AnotType.fst.expected | 2 +- tests/error-messages/NegativeTests.Neg.fst.expected | 4 ++-- .../error-messages/NegativeTests.Positivity.fst.expected | 8 ++++---- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/error-messages/AnotType.fst.expected b/tests/error-messages/AnotType.fst.expected index 0eaf6bb5bfb..61faa2d542a 100644 --- a/tests/error-messages/AnotType.fst.expected +++ b/tests/error-messages/AnotType.fst.expected @@ -1,5 +1,5 @@ >> Got issues: [ -AnotType.fst(19,0-19,19): (Error 309) Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers +AnotType.fst(19,5-19,7): (Error 309) Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers >>] >> Got issues: [ AnotType.fst(27,14-27,16): (Error 189) Expected expression of type "Type0"; got expression "AnotType.tb" of type "Type" diff --git a/tests/error-messages/NegativeTests.Neg.fst.expected b/tests/error-messages/NegativeTests.Neg.fst.expected index 94a1ad7ac6b..78ac8890724 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.expected @@ -26,10 +26,10 @@ NegativeTests.Neg.fst(50,45-50,47): (Error 19) Subtyping check failed; expected NegativeTests.Neg.fst(55,25-55,26): (Error 19) Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query. Use --query_stats for more details. (see also prims.fst(659,18-659,24)) >>] >> Got issues: [ -NegativeTests.Neg.fst(59,0-60,17): (Error 309) Type annotation _: Type0{NegativeTests.Neg.phi_1510} for inductive NegativeTests.Neg.t is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers +NegativeTests.Neg.fst(59,5-59,6): (Error 309) Type annotation _: Type0{NegativeTests.Neg.phi_1510} for inductive NegativeTests.Neg.t is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers >>] >> Got issues: [ -NegativeTests.Neg.fst(63,0-63,32): (Error 309) Type annotation _: Type{Prims.l_False} for inductive NegativeTests.Neg.t2 is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers +NegativeTests.Neg.fst(63,5-63,7): (Error 309) Type annotation _: Type{Prims.l_False} for inductive NegativeTests.Neg.t2 is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers >>] NegativeTests.Neg.fst(18,4-18,5): (Warning 240) NegativeTests.Neg.x is declared but no definition was found; add an 'assume' if this is intentional NegativeTests.Neg.fst(22,4-22,5): (Warning 240) NegativeTests.Neg.y is declared but no definition was found; add an 'assume' if this is intentional diff --git a/tests/error-messages/NegativeTests.Positivity.fst.expected b/tests/error-messages/NegativeTests.Positivity.fst.expected index a8bf9ae7e24..472bf1b1f58 100644 --- a/tests/error-messages/NegativeTests.Positivity.fst.expected +++ b/tests/error-messages/NegativeTests.Positivity.fst.expected @@ -1,8 +1,8 @@ >> Got issues: [ -NegativeTests.Positivity.fst(22,5-23,26): (Error 3) Inductive type NegativeTests.Positivity.t1 does not satisfy the strict positivity condition +NegativeTests.Positivity.fst(22,10-22,12): (Error 3) Inductive type NegativeTests.Positivity.t1 does not satisfy the strict positivity condition >>] >> Got issues: [ -NegativeTests.Positivity.fst(37,5-38,26): (Error 3) Inductive type NegativeTests.Positivity.t5 does not satisfy the strict positivity condition +NegativeTests.Positivity.fst(37,10-37,12): (Error 3) Inductive type NegativeTests.Positivity.t5 does not satisfy the strict positivity condition >>] >> Got issues: [ NegativeTests.Positivity.fst(49,4-49,7): (Error 3) Type NegativeTests.Positivity.t7 is not strictly positive since it instantiates a non-uniformly recursive parameter or index NegativeTests.Positivity.t7 of NegativeTests.Positivity.t6 (see also NegativeTests.Positivity.fst(49,12-49,14)) @@ -11,10 +11,10 @@ NegativeTests.Positivity.fst(49,4-49,7): (Error 3) Type NegativeTests.Positivity NegativeTests.Positivity.fst(54,4-54,7): (Error 3) Type NegativeTests.Positivity.t8 is not strictly positive since it instantiates a non-uniformly recursive parameter or index NegativeTests.Positivity.t8 of NegativeTests.Positivity.t6 (see also NegativeTests.Positivity.fst(54,16-54,18)) >>] >> Got issues: [ -NegativeTests.Positivity.fst(61,5-62,23): (Error 3) Inductive type NegativeTests.Positivity.t10 does not satisfy the strict positivity condition +NegativeTests.Positivity.fst(61,10-61,13): (Error 3) Inductive type NegativeTests.Positivity.t10 does not satisfy the strict positivity condition >>] >> Got issues: [ -NegativeTests.Positivity.fst(66,5-67,30): (Error 3) Inductive type NegativeTests.Positivity.t11 does not satisfy the strict positivity condition +NegativeTests.Positivity.fst(66,10-66,13): (Error 3) Inductive type NegativeTests.Positivity.t11 does not satisfy the strict positivity condition >>] Verified module: NegativeTests.Positivity All verification conditions discharged successfully