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 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 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