aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Instantiate mvars during echo

This commit is contained in:
Leni Aniva 2024-03-31 17:09:24 -07:00
parent 2511573a82
commit 6f85c262cf
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 11 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Pantograph/Library.lean
View File

@ -116,7 +116,7 @@ def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) :=
| .ok syn => pure syn
match ← elabType syn with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr
| .ok expr => return .ok (← Lean.instantiateMVars expr)
/-- This must be a TermElabM since the parsed expr contains extra information -/
def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
@ -130,7 +130,7 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E
| .ok syn => pure syn
match ← elabTerm syn expectedType? with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr
| .ok expr => return .ok (← Lean.instantiateMVars expr)
@[export pantograph_expr_echo_m]
def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):

11
Test/Library.lean
View File

@ -20,9 +20,16 @@ def test_expr_echo: IO LSpec.TestSeq := do
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
}))
let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := {})
let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := { pp? := "(p : Prop) ×' p" }, expr := { pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩" }
type := {
pp? := "(p : Prop) ×' p",
sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
},
expr := {
pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
}
}))
return tests
runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner