From b006ba325c986c6c359d77878c818b601bd3a419 Mon Sep 17 00:00:00 2001
From: Alissa Tung <alissa-tung@outlook.com>
Date: Sun, 10 Nov 2024 02:05:14 +0800
Subject: [PATCH] test-set-b: *

---
 flake.nix                          |   3 +-
 nix/bootstrap.nix                  |   3 +-
 src/Lean/Analyser.lean             |   7 ++
 src/Lean/Analyser/Data.lean        |  17 +++++
 src/Lean/Analyser/ExprToJson.lean  | 106 +++++++++++++++++++++++++++
 src/Lean/Analyser/Flags.lean       |  13 ++++
 src/Lean/Analyser/IO.lean          |  53 ++++++++++++++
 src/Lean/Analyser/Options.lean     |   9 +++
 src/Lean/Analyser/Prelude.lean     |  13 ++++
 src/Lean/Analyser/Trace.lean       |  12 +++
 src/Lean/CoreM.lean                |   2 +-
 src/Lean/Elab/Command.lean         |  20 ++++-
 src/Lean/Elab/Tactic/ElabTerm.lean | 114 ++++++++++++++++++++++++++++-
 src/Lean/Elab/Term.lean            |   8 ++
 14 files changed, 375 insertions(+), 5 deletions(-)
 create mode 100644 src/Lean/Analyser.lean
 create mode 100644 src/Lean/Analyser/Data.lean
 create mode 100644 src/Lean/Analyser/ExprToJson.lean
 create mode 100644 src/Lean/Analyser/Flags.lean
 create mode 100644 src/Lean/Analyser/IO.lean
 create mode 100644 src/Lean/Analyser/Options.lean
 create mode 100644 src/Lean/Analyser/Prelude.lean
 create mode 100644 src/Lean/Analyser/Trace.lean

diff --git a/flake.nix b/flake.nix
index e31257f8c5..4b582a0005 100644
--- a/flake.nix
+++ b/flake.nix
@@ -33,7 +33,8 @@
           buildInputs = with pkgs; [
             cmake gmp libuv ccache cadical pkg-config
             lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-            gdb
+            # gdb
+            postgresql
             tree  # for CI
           ];
           # https://github.com/NixOS/nixpkgs/issues/60919
diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index c29a902593..7e3bc92cda 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -2,7 +2,8 @@
   stdenv, lib, cmake, pkg-config, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
   ... } @ args:
 with builtins;
-lib.warn "The Nix-based build is deprecated" rec {
+# lib.warn "The Nix-based build is deprecated" rec {
+rec {
   inherit stdenv;
   sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
   buildCMake = args: stdenv.mkDerivation ({
diff --git a/src/Lean/Analyser.lean b/src/Lean/Analyser.lean
new file mode 100644
index 0000000000..a364129186
--- /dev/null
+++ b/src/Lean/Analyser.lean
@@ -0,0 +1,7 @@
+import Lean.Analyser.Data
+import Lean.Analyser.Flags
+import Lean.Analyser.IO
+import Lean.Analyser.Options
+import Lean.Analyser.Trace
+import Lean.Analyser.Prelude
+import Lean.Analyser.ExprToJson
diff --git a/src/Lean/Analyser/Data.lean b/src/Lean/Analyser/Data.lean
new file mode 100644
index 0000000000..8bd78c7865
--- /dev/null
+++ b/src/Lean/Analyser/Data.lean
@@ -0,0 +1,17 @@
+import Lean.Data.Position
+
+open Lean
+
+namespace Analyser
+
+structure Range where
+  startPosition : Option Position
+  endPosition : Option Position
+deriving ToJson
+
+def Range.get (stx : Syntax) {m : Type -> Type} [Monad m]
+  [MonadFileMap m] : m Range := do
+    let fileMap <- getFileMap
+    let startPosition := stx.getPos? <&> fileMap.toPosition
+    let endPosition := stx.getTailPos? <&> fileMap.toPosition
+    return { startPosition, endPosition }
diff --git a/src/Lean/Analyser/ExprToJson.lean b/src/Lean/Analyser/ExprToJson.lean
new file mode 100644
index 0000000000..d1d260e855
--- /dev/null
+++ b/src/Lean/Analyser/ExprToJson.lean
@@ -0,0 +1,106 @@
+prelude
+import Lean.Meta.Tactic.Util
+import Lean.Elab.Term
+
+open Lean Meta Elab Tactic IO
+
+inductive YourExpr where
+  | bvar (deBruijnIndex : Nat)
+  | fvar (fvarId : String)
+  | mvar (mvarId : String)
+  | sort (u : String)
+  | const (declName : String) (us : List String)
+  | app (fn : YourExpr) (arg : YourExpr)
+  | lam (binderName : String) (binderType : YourExpr) (body : YourExpr) (binderInfo : String)
+  | forallE (binderName : String) (binderType : YourExpr) (body : YourExpr) (binderInfo : String)
+  | letE (declName : String) (type : YourExpr) (value : YourExpr) (body : YourExpr) (nonDep : Bool)
+  | lit (literal : String)
+  | mdata (data : String) (expr : YourExpr)
+  | proj (typeName : String) (idx : Nat) (struct : YourExpr)
+  deriving ToJson, FromJson, Repr, Inhabited
+
+namespace ExprConversionNonRecNoMemo
+
+structure Frame where
+  node         : Expr
+  childResults : Array YourExpr
+  remaining    : List Expr
+  deriving Inhabited
+
+def getChildren (e : Expr) : List Expr :=
+  match e with
+  | Expr.app f a           => [f, a]
+  | Expr.lam _ binderType body _         => [binderType, body]
+  | Expr.forallE _ binderType body _       => [binderType, body]
+  | Expr.letE _ type value body _          => [type, value, body]
+  | Expr.mdata _ expr      => [expr]
+  | Expr.proj _ _ struct   => [struct]
+  | _                      => []
+
+def reconstruct (e : Expr) (children : List YourExpr) : YourExpr :=
+  match e with
+  | Expr.bvar idx           => YourExpr.bvar idx
+  | Expr.fvar fvarId        => YourExpr.fvar ((repr fvarId).pretty)
+  | Expr.mvar mvarId        => YourExpr.mvar ((repr mvarId).pretty)
+  | Expr.sort lvl           => YourExpr.sort ((repr lvl).pretty)
+  | Expr.const declName us  => YourExpr.const (declName.toString) (us.map (fun lvl => (repr lvl).pretty))
+  | Expr.app _ _            =>
+      match children with
+      | [f', a'] => YourExpr.app f' a'
+      | _        => panic "Unexpected children count in app"
+  | Expr.lam binderName _ _ binderInfo  =>
+      match children with
+      | [binderType', body'] => YourExpr.lam (binderName.toString) binderType' body' ((repr binderInfo).pretty)
+      | _                    => panic "Unexpected children count in lam"
+  | Expr.forallE binderName _ _ binderInfo =>
+      match children with
+      | [binderType', body'] => YourExpr.forallE (binderName.toString) binderType' body' ((repr binderInfo).pretty)
+      | _                    => panic "Unexpected children count in forallE"
+  | Expr.letE declName _ _ _ nonDep       =>
+      match children with
+      | [type', value', body'] => YourExpr.letE (declName.toString) type' value' body' nonDep
+      | _                      => panic "Unexpected children count in letE"
+  | Expr.lit lit            => YourExpr.lit ((repr lit).pretty)
+  | Expr.mdata data _       =>
+      match children with
+      | [expr'] => YourExpr.mdata ((repr data).pretty) expr'
+      | _       => panic "Unexpected children count in mdata"
+  | Expr.proj typeName idx _  =>
+      match children with
+      | [struct'] => YourExpr.proj (typeName.toString) idx struct'
+      | _         => panic "Unexpected children count in proj"
+
+
+def exprToYourExprIter (e : Expr) (maxDepth : Nat) : IO YourExpr := do
+  let mut stack : List Frame := []
+  stack := [{ node := e, childResults := #[], remaining := getChildren e }]
+  while !stack.isEmpty do
+    if stack.length > maxDepth then
+      throw $ IO.userError "Iteration depth exceeded threshold"
+    let top := stack.head!
+    match top.remaining with
+    | child :: rest =>
+         stack := { top with remaining := rest } :: stack.tail!
+         stack := { node := child, childResults := #[], remaining := getChildren child } :: stack
+    | [] =>
+         let result := reconstruct top.node (top.childResults.toList)
+         stack := stack.tail!
+         if stack.isEmpty then
+           return result
+         else
+           let parent := stack.head!
+           let updatedParent := { parent with childResults := parent.childResults.push result }
+           stack := updatedParent :: stack.tail!
+  unreachable!
+
+end ExprConversionNonRecNoMemo
+
+def yourExprToJson (expr : YourExpr) : IO String :=
+  let exprJson := toJson expr |> toString
+  let exprJson := exprJson.replace "\\n" ""
+  let exprJson := exprJson.replace " " ""
+  pure exprJson
+
+def exprToJson (expr : Expr) : IO String := do
+  let yourExpr ← ExprConversionNonRecNoMemo.exprToYourExprIter expr 1000
+  yourExprToJson yourExpr
diff --git a/src/Lean/Analyser/Flags.lean b/src/Lean/Analyser/Flags.lean
new file mode 100644
index 0000000000..919fa4aacd
--- /dev/null
+++ b/src/Lean/Analyser/Flags.lean
@@ -0,0 +1,13 @@
+import Lean.Analyser.Options
+
+open Lean
+
+variable {m : Type -> Type} [Monad m] [MonadOptions m] [MonadLiftT BaseIO m]
+
+def analyser_services_push : m Bool := do
+  return analyser.services.push.get (<- getOptions)
+    || .some "1" == (<- IO.getEnv "ANALYSER_SERVICES_PUSH")
+
+def analyser_services_trace : m Bool := do
+  return analyser.services.trace.get (<- getOptions)
+    || .some "1" == (<- IO.getEnv "ANALYSER_SERVICES_TRACE")
diff --git a/src/Lean/Analyser/IO.lean b/src/Lean/Analyser/IO.lean
new file mode 100644
index 0000000000..6a924f361d
--- /dev/null
+++ b/src/Lean/Analyser/IO.lean
@@ -0,0 +1,53 @@
+import Lean.Analyser.Trace
+import Lean.Data.Json.FromToJson
+
+open Lean
+
+inductive PsqlPushDataMethod where
+| tacticStep
+
+instance : ToString PsqlPushDataMethod where
+  toString
+  | .tacticStep => "tactic_step"
+
+private def psqlPushData (method : PsqlPushDataMethod) (data : Json) : IO UInt32 := do
+  let child <- IO.Process.spawn
+    { cmd := "psql"
+    , args :=
+      #[ "-q"
+       , "-U", "postgres"
+       , "-h", "127.0.0.1"
+       , "-p", "5595"
+       , "-d", "pfdb"
+       , "-f", "-"
+       ]
+    , stdin := IO.Process.Stdio.piped
+    , stdout := IO.Process.Stdio.null
+    , stderr := IO.Process.Stdio.null
+    }
+  let (stdin, child) <- child.takeStdin
+  stdin.putStr s!"insert into \"{method}\" (data) values ((to_jsonb($PG_RAW${data}$PG_RAW$::text)->>0)::jsonb);\n"
+  stdin.flush
+  child.wait
+
+private def psqlPushDataWithRetry (acc : Nat) (method : PsqlPushDataMethod) (data : Json) : IO UInt32 :=
+  match acc with
+  | .zero => psqlPushData method data
+  | .succ acc => do
+    if 0 == (<- psqlPushData method data)
+      then return 0
+      else psqlPushDataWithRetry acc method data
+
+variable {m : Type -> Type} [Monad m]
+  [MonadOptions m] [MonadLog m] [AddMessageContext m]
+  [MonadLiftT IO m] [MonadLiftT BaseIO m]
+
+variable {d : Type} [ToJson d]
+
+def pushData (method : PsqlPushDataMethod) (data : d) : m Unit := do
+  let data := toJson data
+  if <- analyser_services_push then
+    let code <- psqlPushDataWithRetry 2 method data
+    if code != 0 then
+      logWarning s!"failed to push data: method = `{method}`, data = `{data}`"
+  traceInfo s!"{method}: {data}"
diff --git a/src/Lean/Analyser/Options.lean b/src/Lean/Analyser/Options.lean
new file mode 100644
index 0000000000..ed840f5b81
--- /dev/null
+++ b/src/Lean/Analyser/Options.lean
@@ -0,0 +1,9 @@
+import Lean.Data.Options
+
+register_option analyser.services.push : Bool := {
+  defValue := false
+}
+
+register_option analyser.services.trace : Bool := {
+  defValue := false
+}
diff --git a/src/Lean/Analyser/Prelude.lean b/src/Lean/Analyser/Prelude.lean
new file mode 100644
index 0000000000..d1ebfe243f
--- /dev/null
+++ b/src/Lean/Analyser/Prelude.lean
@@ -0,0 +1,13 @@
+import Lean.Syntax
+
+open Lean
+
+private def Syntax.before.h (x stx : Syntax) : Option Syntax := do
+  if x == stx then return .missing
+  let xRange <- x.getRange?
+  let stxRange <- stx.getRange?
+  if xRange.start <= stxRange.start then return .missing
+  .none
+
+def Syntax.before (xs : Syntax) (x : Syntax) : Option Syntax := do
+  return Syntax.replaceM (m := Id) (Syntax.before.h x) xs
diff --git a/src/Lean/Analyser/Trace.lean b/src/Lean/Analyser/Trace.lean
new file mode 100644
index 0000000000..e571c63b6b
--- /dev/null
+++ b/src/Lean/Analyser/Trace.lean
@@ -0,0 +1,12 @@
+import Lean.Log
+import Lean.Analyser.Flags
+
+open Lean
+
+variable {m : Type -> Type} [Monad m]
+  [MonadOptions m] [MonadLiftT BaseIO m]
+  [MonadLog m] [AddMessageContext m]
+
+def traceInfo (msgData : MessageData) : m Unit := do
+  if <- analyser_services_trace then
+    logInfo msgData
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index db43afd0ff..2060f16094 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -27,7 +27,7 @@ register_builtin_option diagnostics.threshold : Nat := {
 }
 
 register_builtin_option maxHeartbeats : Nat := {
-  defValue := 200000
+  defValue := 2000000
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 48a5f37e3c..5a5637c83d 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -691,6 +691,15 @@ variable (n : Nat)
 ```
 -/
 def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
+
+----------------------------------------------------------------------------------------------------
+-- begin analyser hack
+
+  let commandSyntax := (<- read).ref
+
+-- end analyser hack
+----------------------------------------------------------------------------------------------------
+
   let scope ← getScope
   liftTermElabM <|
     Term.withAutoBoundImplicit <|
@@ -701,7 +710,16 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
         let mut sectionFVars := {}
         for uid in scope.varUIds, x in xs do
           sectionFVars := sectionFVars.insert uid x
-        withReader ({ · with sectionFVars := sectionFVars }) do
+
+----------------------------------------------------------------------------------------------------
+-- begin analyser hack
+
+        -- withReader ({ · with sectionFVars := sectionFVars }) do
+        withReader ({ · with sectionFVars, commandSyntax }) do
+
+-- end analyser hack
+----------------------------------------------------------------------------------------------------
+
           -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
           -- So, we use `Core.resetMessageLog`.
           Core.resetMessageLog
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index a599dfc05b..a2c93cac90 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -13,6 +13,8 @@ import Lean.Meta.Tactic.Rename
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.Config
 import Lean.Elab.SyntheticMVars
+import Lean.Meta.Reduce
+import Lean.Meta.ExprTraverse
 
 namespace Lean.Elab.Tactic
 open Meta
@@ -94,11 +96,121 @@ def closeMainGoalUsing (tacName : Name) (x : Expr → Name → TacticM Expr) (ch
       pushGoal mvarId
       throw ex)
 
+----------------------------------------------------------------------------------------------------
+
+def tryOption {a : Type _} (xs : TacticM a) : TacticM $ Option a := do
+  try return Option.some (<- xs)
+    catch _ => return none
+
+def _root_.Lean.Syntax.getAppFn (stx : Syntax) (expr : Expr) : TacticM (Option Name) := do
+  let name <- tryOption (resolveGlobalConstNoOverload stx)
+  let .none := name | return name
+  let .const name _ := expr.getAppFn | return .none
+  return .some name
+
+structure TacticStepMeta where
+  declName : Option String
+  uri : String
+  range : Analyser.Range
+
+def TacticStepMeta.get (stx : Syntax) : TacticM TacticStepMeta := do
+  return { declName := (<- (read : TermElabM _)).declName?.map toString
+         , uri := <- getFileName
+         , range := (<- Analyser.Range.get stx)
+         }
+
+structure TacticStep extends TacticStepMeta where
+  appFnName : String
+  mainGoalTypeJson : String
+  mainGoalTypeJsonSimp : String
+  mainGoalTypeStr : String
+  exactStxReprint : String
+  commandSyntaxKind : String
+deriving ToJson
+
+def execClear (decl : LocalDecl) : TacticM Unit := do
+  let fvarIds := #[decl.fvarId]
+  let fvarIds ← withMainContext <| sortFVarIds fvarIds
+  for fvarId in fvarIds.reverse do
+    withMainContext do
+      let mvarId ← (← getMainGoal).clear fvarId
+      replaceMainGoal [mvarId]
+
+def withoutModifyingState! {a : Type _} (xs : TacticM a) : TacticM $ Option a := do
+  let state <- saveState
+  let x <- try
+    xs
+  catch _ => return .none
+  finally
+    state.restore (restoreInfo := true)
+  return pure x
+
+def _root_.Bool.to_option (b : Bool) :=
+  if b then
+    Option.some ()
+  else
+    .none
+
+def appendAfterOrig (orig : Expr) (newBinders : Array (Name × Expr)) : MetaM Expr := do
+  forallTelescope orig fun origFVars target => do
+    withLocalDeclsDND newBinders fun newFVars => do
+      let allFVars := (origFVars.toList ++ newFVars.toList).toArray
+      mkForallFVars allFVars target
+
+def getTacticStepData (e : TSyntax `term) (expr : Expr) : TacticM $ Option (Name × Expr) := return Option.join $ <- withoutModifyingState! do
+  let mainGoal <- getMainGoal
+  let guard := Option.join $ <- withoutModifyingState! do
+    try
+      let expr <- withMainContext do elabTermEnsuringType e (<- mainGoal.getType)
+      closeMainGoalUsing `exact fun _ _ => return expr
+      return (<- mainGoal.isAssigned).to_option
+    catch _ => return .none
+  let .some () := guard | return .none
+
+  return Option.join $ <- withoutModifyingState! do
+    let .some appFn <- e.raw.getAppFn expr | return Option.none
+    let mainGoalType <- (<- getMainGoal).getType
+    let (_fvars, binders, _target) <- forallMetaTelescopeReducing (<- getConstInfo appFn).type
+    let appArgsInfo <- expr.getAppArgs.mapM fun appArg => do
+      let x <- withMainContext do withTransparency TransparencyMode.all do inferType appArg
+      let x <- instantiateMVars x
+      return (Name.anonymous, x)
+    let appArgsInfo := (binders.zip appArgsInfo).filter fun (binderInfo, _, _) => binderInfo == BinderInfo.default
+    let appArgsInfo := appArgsInfo.map fun (_, y, z) => (y, z)
+    let mainGoalType <- appendAfterOrig mainGoalType appArgsInfo
+
+    return .some (appFn, mainGoalType)
+
+partial def reduceAllRec (expr : Expr) : MetaM Expr := do
+  let expr <- reduceAll expr
+  traverseChildren reduceAllRec expr
+
+def pushTacticStepData (stx : Syntax) (appFn : Name) (mainGoalType : Expr) : TacticM Unit := do
+  let .some commandSyntaxKind := (<- read (m := TermElabM)).commandSyntax.map fun commandSyntax => commandSyntax[1].getKind | return
+  let .some mainGoalTypeJsonSimp <- withoutModifyingState! do reduceAllRec mainGoalType | return
+  let .some exactStxReprint := stx.reprint | return
+  pushData (d := TacticStep) .tacticStep
+    { <- TacticStepMeta.get stx with
+      appFnName := (s!"{appFn}")
+    , mainGoalTypeJson := (<- exprToJson mainGoalType)
+    , mainGoalTypeJsonSimp := (<- exprToJson mainGoalTypeJsonSimp)
+    , mainGoalTypeStr := s!"{<- ppExpr mainGoalType}"
+    , exactStxReprint
+    , commandSyntaxKind := s!"{commandSyntaxKind}"
+    }
+
 @[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
   match stx with
-  | `(tactic| exact $e) => closeMainGoalUsing `exact fun type _ => elabTermEnsuringType e type
+  | `(tactic| exact $e) => do
+    let expr <- withMainContext do elabTermEnsuringType e (<- (<- getMainGoal).getType)
+    let () <- match <- getTacticStepData e expr with
+    | .some (appFn, mainGoalType) => pushTacticStepData stx appFn mainGoalType
+    | _ => pure ()
+    closeMainGoalUsing `exact fun _ _ => return expr
   | _ => throwUnsupportedSyntax
 
+----------------------------------------------------------------------------------------------------
+
 def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := do
   let mctx ← getMCtx
   return mvarIds.qsort fun mvarId₁ mvarId₂ =>
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 065422c105..425ee60e1e 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -331,6 +331,14 @@ structure Context where
   -/
   checkDeprecated : Bool := true
 
+----------------------------------------------------------------------------------------------------
+-- begin analyser hack
+
+  commandSyntax : Option Syntax := .none
+
+-- end analyser hack
+----------------------------------------------------------------------------------------------------
+
 abbrev TermElabM := ReaderT Context $ StateRefT State MetaM
 abbrev TermElab  := Syntax → Option Expr → TermElabM Expr
 
-- 
2.39.5 (Apple Git-154)

