From a62ac51c37ad5dde6c3e850aaaf1e9b9265ec652 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 22:11:37 -0800 Subject: [PATCH] chore: Remove all redundant filenames --- Pantograph/Goal.lean | 10 ++++------ Test/Common.lean | 6 +++--- Test/Tactic/MotivatedApply.lean | 6 +++--- Test/Tactic/NoConfuse.lean | 6 +++--- Test/Tactic/Prograde.lean | 2 +- 5 files changed, 14 insertions(+), 16 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index be745f4..8d29aa8 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -10,8 +10,6 @@ import Lean namespace Pantograph open Lean -def filename: String := "" - /-- Represents an interconnected set of metavariables, or a state in proof search -/ @@ -224,7 +222,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str (env := ← MonadEnv.getEnv) (catName := if state.isConv then `conv else `tactic) (input := tactic) - (fileName := filename) with + (fileName := ← getFileName) with | .ok stx => pure $ stx | .error error => return .parseError error state.tryTacticM goal $ Elab.Tactic.evalTactic tactic @@ -236,7 +234,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin (env := ← MonadEnv.getEnv) (catName := `term) (input := expr) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalAssign expr @@ -250,7 +248,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St (env := ← MonadEnv.getEnv) (catName := `term) (input := type) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalLet binderName.toName type @@ -337,7 +335,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) (env := state.env) (catName := `term) (input := pred) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error goal.checkNotAssigned `GoalState.tryCalc diff --git a/Test/Common.lean b/Test/Common.lean index 212e164..53adaa0 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -95,19 +95,19 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq) def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e -def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do +def strToTermSyntax (s: String): CoreM Syntax := do let .ok stx := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) | panic! s!"Failed to parse {s}" + (fileName := ← getFileName) | panic! s!"Failed to parse {s}" return stx def parseSentence (s: String): Elab.TermElabM Expr := do let stx ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" Elab.Term.elabTerm (stx := stx) .none diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 4fb05e3..61d7d6c 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -28,7 +28,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@List.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -74,7 +74,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" let expr ← parseSentence expr diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index ac277e2..93f0606 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -15,7 +15,7 @@ def test_nat : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -32,7 +32,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 132718a..b3347cb 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -15,7 +15,7 @@ def test_define : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "Or.inl h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic