feat: Instantiation tests
Note that delay assigned metavariables are not instantiated.
This commit is contained in:
parent
aeed233846
commit
bc83a5732e
|
@ -127,7 +127,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
|
|||
| .error e => return .error e
|
||||
| .ok expr => pure expr
|
||||
try
|
||||
let type ← Lean.Meta.inferType expr
|
||||
let type ← instantiateAll (← Lean.Meta.inferType expr)
|
||||
return .ok {
|
||||
type := (← serialize_expression options type),
|
||||
expr := (← serialize_expression options expr)
|
||||
|
@ -171,9 +171,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
|
|||
state.restoreMetaM
|
||||
return {
|
||||
root? := ← state.rootExpr?.mapM (λ expr => do
|
||||
serialize_expression options (← unfoldAuxLemmas expr)),
|
||||
serialize_expression options (← instantiateAll expr)),
|
||||
parent? := ← state.parentExpr?.mapM (λ expr => do
|
||||
serialize_expression options (← unfoldAuxLemmas expr)),
|
||||
serialize_expression options (← instantiateAll expr)),
|
||||
}
|
||||
runMetaM metaM
|
||||
|
||||
|
|
|
@ -18,6 +18,10 @@ namespace Pantograph
|
|||
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
|
||||
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 ---
|
||||
|
||||
/-- Read syntax object from string -/
|
||||
|
|
|
@ -13,6 +13,27 @@ abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
|
|||
def addTest (test: LSpec.TestSeq): TestM Unit := do
|
||||
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
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let syn? := syntax_from_str env expr
|
||||
|
@ -140,8 +161,9 @@ def test_m_couple_simp: TestM Unit := do
|
|||
return ()
|
||||
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)))")
|
||||
let rootStr: String := toString (← Lean.Meta.ppExpr (← 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)))")
|
||||
let unfoldedRoot ← unfoldAuxLemmas root
|
||||
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 ()
|
||||
|
||||
def test_proposition_generation: TestM Unit := do
|
||||
|
@ -252,6 +274,7 @@ def suite: IO LSpec.TestSeq := do
|
|||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
let tests := [
|
||||
("Instantiate", test_instantiate_mvar),
|
||||
("2 < 5", test_m_couple),
|
||||
("2 < 5", test_m_couple_simp),
|
||||
("Proposition Generation", test_proposition_generation),
|
||||
|
|
Loading…
Reference in New Issue