Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ToSyntax: improve some ranges #3014

Merged
merged 4 commits into from
Aug 14, 2023
Merged

ToSyntax: improve some ranges #3014

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8be5721
ToSyntax: improve some ranges
mtzguido Aug 10, 2023
4f870e4
snap
mtzguido Aug 10, 2023
3626877
error-messages: update, errors now point to type names
mtzguido Aug 10, 2023
558402c
Merge branch 'master' into guido_ranges
mtzguido Aug 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 35 additions & 20 deletions ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

16 changes: 8 additions & 8 deletions src/tosyntax/FStar.ToSyntax.ToSyntax.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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; }))))
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/error-messages/AnotType.fst.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
4 changes: 2 additions & 2 deletions tests/error-messages/NegativeTests.Neg.fst.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions tests/error-messages/NegativeTests.Positivity.fst.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))
Expand All @@ -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