From d18305297db4e3040f4367c640609b4bed18845a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Oct 2019 10:49:01 -0700
Subject: [PATCH] feat: add `Expr.getAppRevArgs`

---
 library/Init/Lean/Expr.lean |  7 +++++++
 tests/lean/run/expr1.lean   | 16 ++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 tests/lean/run/expr1.lean

diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean
index 2dea39b678..beea60f7aa 100644
--- a/library/Init/Lean/Expr.lean
+++ b/library/Init/Lean/Expr.lean
@@ -168,6 +168,13 @@ let dummy := Expr.sort Level.zero;
 let nargs := e.getAppNumArgs;
 getAppArgsAux e (mkArray nargs dummy) (nargs-1)
 
+private def getAppRevArgsAux : Expr → Array Expr → Array Expr
+| Expr.app f a, as => getAppRevArgsAux f (as.push a)
+| _,            as => as
+
+@[inline] def getAppRevArgs (e : Expr) : Array Expr :=
+getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs)
+
 def isAppOf (e : Expr) (n : Name) : Bool :=
 match e.getAppFn with
 | Expr.const c _ => c == n
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
new file mode 100644
index 0000000000..0fa7b1173f
--- /dev/null
+++ b/tests/lean/run/expr1.lean
@@ -0,0 +1,16 @@
+import Init.Lean.Expr
+open Lean
+
+def tst1 : IO Unit :=
+do let f   := Expr.const `f [];
+   let a   := Expr.const `a [];
+   let b   := Expr.const `b [];
+   let t   := mkApp f #[a, b, b];
+   let as₁ := t.getAppArgs;
+   let as₂ := t.getAppRevArgs;
+   IO.println as₁;
+   IO.println as₂;
+   unless (as₁.reverse == as₂) $ throw "failed";
+   pure ()
+
+#eval tst1