fix: Instantiation causes infinite loop #54

Merged
aniva merged 2 commits from output/expr into dev 2024-03-31 16:43:53 -07:00
3 changed files with 5 additions and 9 deletions

View File

@ -64,7 +64,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
else .none,
valueDependency? := ← if args.dependency?.getD false
then info.value?.mapM (λ e => do
let e ← (unfoldAuxLemmas e).run'
let e ← unfoldAuxLemmas e
pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
else pure (.none),
module? := module?

View File

@ -127,7 +127,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
| .error e => return .error e
| .ok expr => pure expr
try
let type ← instantiateAll (← Lean.Meta.inferType expr)
let type ← unfoldAuxLemmas (← 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 (← instantiateAll expr)),
serialize_expression options (← unfoldAuxLemmas expr)),
parent? := ← state.parentExpr?.mapM (λ expr => do
serialize_expression options (← instantiateAll expr)),
serialize_expression options (← unfoldAuxLemmas expr)),
}
runMetaM metaM

View File

@ -15,13 +15,9 @@ def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxL
namespace Pantograph
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM 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 -/