From 9f0e4605e1c8816dbf5ed3e9e893b25e9a2be4a3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 26 Jan 2024 00:17:59 +0100
Subject: Improve the Lean backend

---
 backends/lean/Base/Progress/Base.lean | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'backends/lean/Base/Progress/Base.lean')

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 0ad16ab6..935af3f5 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -82,17 +82,21 @@ section Methods
     -- Destruct the equality
     let (mExpr, ret) ← destEq th.consumeMData
     trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}"
-    -- Destruct the monadic application to dive into the bind, if necessary (this
-    -- is for when we use `withPSpec` inside of the `progress` tactic), and
-    -- destruct the application to get the function name
-    mExpr.consumeMData.withApp fun mf margs => do
-    trace[Progress] "After stripping the arguments of the monad expression:\n- mf: {mf}\n- margs: {margs}"
-    let (fArgsExpr, f, args) ← do
+    -- Recursively destruct the monadic application to dive into the binds,
+    -- if necessary (this is for when we use `withPSpec` inside of the `progress` tactic),
+    -- and destruct the application to get the function name
+    let rec strip_monad mExpr := do
+      mExpr.consumeMData.withApp fun mf margs => do
+      trace[Progress] "After stripping the arguments of the monad expression:\n- mf: {mf}\n- margs: {margs}"
       if mf.isConst ∧ mf.constName = ``Bind.bind then do
         -- Dive into the bind
         let fExpr := (margs.get! 4).consumeMData
-        fExpr.withApp fun f args => pure (fExpr, f, args)
-      else pure (mExpr, mf, margs)
+        -- Recursve
+        strip_monad fExpr
+      else
+        -- No bind
+        pure (mExpr, mf, margs)
+    let (fArgsExpr, f, args) ← strip_monad mExpr
     trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
     if ¬ f.isConst then throwError "Not a constant: {f}"
     -- *Sanity check* (activated if we are analyzing a theorem to register it in a DB)
-- 
cgit v1.2.3


From c709eadb14e2ecd21c9c4a6a9def39334f27552b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 27 Jan 2024 21:26:38 +0100
Subject: Fix a minor issue with the progress tactic

---
 backends/lean/Base/Progress/Base.lean | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'backends/lean/Base/Progress/Base.lean')

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 935af3f5..a64212a5 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -22,8 +22,9 @@ structure PSpecDesc where
   evars : Array Expr
   -- The function applied to its arguments
   fArgsExpr : Expr
-  -- The function
-  fName : Name
+  -- ⊤ if the function is a constant (must be if we are registering a theorem,
+  -- but is not necessarily the case if we are looking at a goal)
+  fIsConst : Bool
   -- The function arguments
   fLevels : List Level
   args : Array Expr
@@ -98,7 +99,12 @@ section Methods
         pure (mExpr, mf, margs)
     let (fArgsExpr, f, args) ← strip_monad mExpr
     trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
-    if ¬ f.isConst then throwError "Not a constant: {f}"
+    let fLevels ← do
+      -- If we are registering a theorem, then the function must be a constant
+      if ¬ f.isConst then
+        if isGoal then pure []
+        else throwError "Not a constant: {f}"
+      else pure f.constLevels!
     -- *Sanity check* (activated if we are analyzing a theorem to register it in a DB)
     -- Check if some existentially quantified variables
     let _ := do
@@ -117,8 +123,8 @@ section Methods
       fvars := fvars
       evars := evars
       fArgsExpr
-      fName := f.constName!
-      fLevels := f.constLevels!
+      fIsConst := f.isConst
+      fLevels
       args := args
       ret := ret
       post := post
-- 
cgit v1.2.3