From 01db46891d92a4d3d3f7eb9646c3912d7bb0057f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 4 Oct 2024 23:11:14 -0700 Subject: [PATCH 1/3] Desugaring: simplify desugaring for App, and respect textual order Missing identifiers on the right of an application are reported first, which is confusing. This patch makes desugaring of applications work left to right, and also removes some unneeded logic when a recursive call was enough. --- src/tosyntax/FStar.ToSyntax.ToSyntax.fst | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index 30ed68488f3..3eea02ba793 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst @@ -1512,17 +1512,11 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an mk (Tm_uinst(head, universes)), aq in aux [] top - | App _ -> - let rec aux args aqs e = match (unparen e).tm with - | App(e, t, imp) when imp <> UnivApp -> - let t, aq = desugar_term_aq env t in - let arg = arg_withimp_t imp t in - aux (arg::args) (aq::aqs) e - | _ -> - let head, aq = desugar_term_aq env e in - S.extend_app_n head args top.range, join_aqs (aq::aqs) - in - aux [] [] top + | App (e, t, imp) -> + let head, aq1 = desugar_term_aq env e in + let t, aq2 = desugar_term_aq env t in + let arg = arg_withimp_t imp t in + S.extend_app head arg top.range, aq1@aq2 | Bind(x, t1, t2) -> let xpat = AST.mk_pattern (AST.PatVar(x, None, [])) (range_of_id x) in From 5963c76519a236824c269d58c0a0ddd76a901aac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 4 Oct 2024 23:14:18 -0700 Subject: [PATCH 2/3] snap --- .../generated/FStar_ToSyntax_ToSyntax.ml | 33 +++++++------------ 1 file changed, 12 insertions(+), 21 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index 90eec7b5514..e289b3f75e6 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -3510,27 +3510,18 @@ and (desugar_term_maybe_top : mk (FStar_Syntax_Syntax.Tm_uinst (head, universes)) in (uu___7, aq)) in aux [] top - | FStar_Parser_AST.App uu___2 -> - let rec aux args aqs e = - let uu___3 = - let uu___4 = unparen e in uu___4.FStar_Parser_AST.tm in - match uu___3 with - | FStar_Parser_AST.App (e1, t, imp) when - imp <> FStar_Parser_AST.UnivApp -> - let uu___4 = desugar_term_aq env t in - (match uu___4 with - | (t1, aq) -> - let arg = arg_withimp_t imp t1 in - aux (arg :: args) (aq :: aqs) e1) - | uu___4 -> - let uu___5 = desugar_term_aq env e in - (match uu___5 with - | (head, aq) -> - let uu___6 = - FStar_Syntax_Syntax.extend_app_n head args - top.FStar_Parser_AST.range in - (uu___6, (join_aqs (aq :: aqs)))) in - aux [] [] top + | FStar_Parser_AST.App (e, t, imp) -> + let uu___2 = desugar_term_aq env e in + (match uu___2 with + | (head, aq1) -> + let uu___3 = desugar_term_aq env t in + (match uu___3 with + | (t1, aq2) -> + let arg = arg_withimp_t imp t1 in + let uu___4 = + FStar_Syntax_Syntax.extend_app head arg + top.FStar_Parser_AST.range in + (uu___4, (FStar_Compiler_List.op_At aq1 aq2)))) | FStar_Parser_AST.Bind (x, t1, t2) -> let xpat = let uu___2 = FStar_Ident.range_of_id x in From cb5cf3b829ead119ae1569251849e757c81eece5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 4 Oct 2024 23:12:39 -0700 Subject: [PATCH 3/3] Add a test --- tests/error-messages/DesugarOrder.fst | 7 +++++++ tests/error-messages/DesugarOrder.fst.expected | 7 +++++++ tests/error-messages/DesugarOrder.fst.json_expected | 5 +++++ 3 files changed, 19 insertions(+) create mode 100644 tests/error-messages/DesugarOrder.fst create mode 100644 tests/error-messages/DesugarOrder.fst.expected create mode 100644 tests/error-messages/DesugarOrder.fst.json_expected diff --git a/tests/error-messages/DesugarOrder.fst b/tests/error-messages/DesugarOrder.fst new file mode 100644 index 00000000000..8cf057a17e6 --- /dev/null +++ b/tests/error-messages/DesugarOrder.fst @@ -0,0 +1,7 @@ +module DesugarOrder + +(* Report 'a' as not found, instead of 'c'. It's clearer +to report errors in textual order. Ideally, we could report all of them +at once (also in order). *) +[@@expect_failure] +let _ = (+) a b c diff --git a/tests/error-messages/DesugarOrder.fst.expected b/tests/error-messages/DesugarOrder.fst.expected new file mode 100644 index 00000000000..098a5082621 --- /dev/null +++ b/tests/error-messages/DesugarOrder.fst.expected @@ -0,0 +1,7 @@ +>> Got issues: [ +* Error 72 at DesugarOrder.fst(7,12-7,13): + - Identifier not found: [a] + +>>] +Verified module: DesugarOrder +All verification conditions discharged successfully diff --git a/tests/error-messages/DesugarOrder.fst.json_expected b/tests/error-messages/DesugarOrder.fst.json_expected new file mode 100644 index 00000000000..297c300a971 --- /dev/null +++ b/tests/error-messages/DesugarOrder.fst.json_expected @@ -0,0 +1,5 @@ +>> Got issues: [ +{"msg":["Identifier not found: [a]"],"level":"Error","range":{"def":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}},"use":{"file_name":"DesugarOrder.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":13}}},"number":72,"ctx":["While desugaring module DesugarOrder"]} +>>] +Verified module: DesugarOrder +All verification conditions discharged successfully