feat: Instantiation tests #52

Merged
aniva merged 2 commits from io/serial into dev 2024-03-30 00:08:33 -07:00
3 changed files with 32 additions and 5 deletions

View File

@ -127,7 +127,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
| .error e => return .error e | .error e => return .error e
| .ok expr => pure expr | .ok expr => pure expr
try try
let type ← Lean.Meta.inferType expr let type ← instantiateAll (← Lean.Meta.inferType expr)
return .ok { return .ok {
type := (← serialize_expression options type), type := (← serialize_expression options type),
expr := (← serialize_expression options expr) expr := (← serialize_expression options expr)
@ -171,9 +171,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
state.restoreMetaM state.restoreMetaM
return { return {
root? := ← state.rootExpr?.mapM (λ expr => do root? := ← state.rootExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)), serialize_expression options (← instantiateAll expr)),
parent? := ← state.parentExpr?.mapM (λ expr => do parent? := ← state.parentExpr?.mapM (λ expr => do
serialize_expression options (← unfoldAuxLemmas expr)), serialize_expression options (← instantiateAll expr)),
} }
runMetaM metaM runMetaM metaM

View File

@ -18,6 +18,10 @@ namespace Pantograph
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
def instantiateAll (e: Lean.Expr) : Lean.MetaM Lean.Expr := do
let e ← unfoldAuxLemmas e
instantiateMVars (← Lean.Meta.whnf e)
--- Input Functions --- --- Input Functions ---
/-- Read syntax object from string -/ /-- Read syntax object from string -/

View File

@ -13,6 +13,27 @@ abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
def addTest (test: LSpec.TestSeq): TestM Unit := do def addTest (test: LSpec.TestSeq): TestM Unit := do
set $ (← get) ++ test set $ (← get) ++ test
-- Tests that all delay assigned mvars are instantiated
def test_instantiate_mvar: TestM Unit := do
let env ← Lean.MonadEnv.getEnv
let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
let syn ← match syntax_from_str env value with
| .ok s => pure $ s
| .error e => do
addTest $ assertUnreachable e
return ()
let expr ← match ← syntax_to_expr syn with
| .ok expr => pure $ expr
| .error e => do
addTest $ assertUnreachable e
return ()
let t ← Lean.Meta.inferType expr
addTest $ LSpec.check "typing" ((toString (← serialize_expression_ast t)) =
"((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
return ()
def startProof (expr: String): TestM (Option GoalState) := do def startProof (expr: String): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let syn? := syntax_from_str env expr let syn? := syntax_from_str env expr
@ -140,8 +161,9 @@ def test_m_couple_simp: TestM Unit := do
return () return ()
let rootStr: String := toString (← Lean.Meta.ppExpr root) let rootStr: String := toString (← Lean.Meta.ppExpr root)
addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))") addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
let rootStr: String := toString (← Lean.Meta.ppExpr (← unfoldAuxLemmas root)) let unfoldedRoot ← unfoldAuxLemmas root
addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))") addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
"Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
return () return ()
def test_proposition_generation: TestM Unit := do def test_proposition_generation: TestM Unit := do
@ -252,6 +274,7 @@ def suite: IO LSpec.TestSeq := do
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
let tests := [ let tests := [
("Instantiate", test_instantiate_mvar),
("2 < 5", test_m_couple), ("2 < 5", test_m_couple),
("2 < 5", test_m_couple_simp), ("2 < 5", test_m_couple_simp),
("Proposition Generation", test_proposition_generation), ("Proposition Generation", test_proposition_generation),