Merge pull request #3523 from mtzguido/desugar_order

Desugaring: simplify desugaring for App, and respect textual order

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

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

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

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