Pantograph/Test/Common.lean

61 lines
1.7 KiB
Plaintext
Raw Permalink Normal View History

2023-11-04 15:00:51 -07:00
import Pantograph.Goal
2024-03-28 00:06:35 -07:00
import Pantograph.Library
import Pantograph.Protocol
import Lean
2023-11-04 15:00:51 -07:00
import LSpec
open Lean
namespace Pantograph
namespace Protocol
/-- Set internal names to "" -/
def Goal.devolatilize (goal: Goal): Goal :=
{
goal with
2023-10-30 14:44:06 -07:00
name := "",
vars := goal.vars.map removeInternalAux,
}
where removeInternalAux (v: Variable): Variable :=
{
v with
name := ""
}
2023-11-04 15:00:51 -07:00
deriving instance DecidableEq, Repr for Expression
deriving instance DecidableEq, Repr for Variable
deriving instance DecidableEq, Repr for Goal
end Protocol
2023-11-04 15:00:51 -07:00
def TacticResult.toString : TacticResult → String
| .success state => s!".success ({state.goals.length} goals)"
| .failure messages =>
let messages := "\n".intercalate messages.toList
s!".failure {messages}"
| .parseError error => s!".parseError {error}"
| .indexError index => s!".indexError {index}"
def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
2024-01-07 14:14:20 -08:00
open Lean
def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
2024-03-28 00:06:35 -07:00
let coreContext: Core.Context ← createCoreContext #[]
2024-01-07 14:14:20 -08:00
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a
def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
runCoreMSeq env metaM.run'
def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
termElabM.run' (ctx := {
declName? := .none,
errToSorry := false,
})
2024-03-28 00:06:35 -07:00
def defaultTermElabMContext: Lean.Elab.Term.Context := {
declName? := some "_pantograph".toName,
errToSorry := false
}
end Pantograph