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

Merge pull request 'feat: Instantiate mvars during echo' (#56) from expr/echo into dev 

Reviewed-on: #56
This commit is contained in:
Leni Aniva 2024-03-31 17:10:29 -07:00
parent 2511573a82 6f85c262cf
commit b1da7f2151
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 | .ok syn => pure syn
match ← elabType syn with match ← elabType syn with
| .error str => return .error $ errorI "elab" str | .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 -/ /-- 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 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 | .ok syn => pure syn
match ← elabTerm syn expectedType? with match ← elabTerm syn expectedType? with
| .error str => return .error $ errorI "elab" str | .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr | .ok expr => return .ok (← Lean.instantiateMVars expr)
@[export pantograph_expr_echo_m] @[export pantograph_expr_echo_m]
def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options): 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 { let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := { pp? := "?m.2" }, expr := { pp? := "?m.3" } 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 { 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 return tests
runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner