From a8e7a1a726c7fe5595c92e5c5b8ff4228628ab65 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:34:52 -0800 Subject: [PATCH 1/2] feat: Erase macro scopes in sexp --- Pantograph/Delate.lean | 6 +++--- Test/Delate.lean | 2 +- Test/Library.lean | 2 +- Test/Proofs.lean | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index be17729..141abd9 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -346,20 +346,20 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM let args := " ".intercalate args pure s!"({fn'} {args})" | .lam binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" | .forallE binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" | .letE name type value body _ => do -- Dependent boolean flag diacarded - let name' := serializeName name + let name' := name.eraseMacroScopes let type' ← self type let value' ← self value let body' ← self body diff --git a/Test/Delate.lean b/Test/Delate.lean index 227ab24..d918dc8 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -32,7 +32,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do let entries: List (String × String) := [ -- This one contains unhygienic variable names which must be suppressed - ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"), + ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"), -- These ones are normal and easy ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"), ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"), diff --git a/Test/Library.lean b/Test/Library.lean index d995374..df1ba4d 100644 --- a/Test/Library.lean +++ b/Test/Library.lean @@ -24,7 +24,7 @@ def test_expr_echo (env: Environment): IO LSpec.TestSeq := do }, 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)))", + sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall a 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))", } })) return tests diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8e3e2a2..02c1bf6 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -282,9 +282,9 @@ def test_or_comm: TestM Unit := do serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" - let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" - let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" - let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" + let caseL := s!"(:lambda h (:fv {fvP}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let caseR := s!"(:lambda h (:fv {fvQ}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))" addTest $ LSpec.test "(2 parent)" (state2parent == s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})") From 44aef76a10a9638caecef46326130ffd7c9fad29 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Nov 2024 12:57:19 -0800 Subject: [PATCH 2/2] refactor: Remove sanitization for mvarId/fvarId --- Pantograph/Delate.lean | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 141abd9..4b3bd51 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -327,11 +327,11 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM -- Lean these are handled using a `#` prefix. pure s!"{deBruijnIndex}" | .fvar fvarId => - let name := ofName fvarId.name + let name := fvarId.name pure s!"(:fv {name})" | .mvar mvarId => do let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv" - let name := ofName mvarId.name + let name := mvarId.name pure s!"(:{pref} {name})" | .sort level => let level := serializeSortLevel level sanitize @@ -387,7 +387,6 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM | .implicit => " :implicit" | .strictImplicit => " :strictImplicit" | .instImplicit => " :instImplicit" - ofName (name: Name) := serializeName name sanitize def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp?: Option String ← match options.printExprPretty with @@ -420,13 +419,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava match localDecl with | .cdecl _ fvarId userName _ _ _ => return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName := toString userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } @@ -436,7 +435,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava let userName := userName.simpMacroScopes let type ← instantiate type return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -450,7 +449,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava else pure $ .none return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -469,7 +468,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava | false => ppVar localDecl return var::acc return { - name := ofName goal.name, + name := goal.name.toString, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serializeExpression options (← instantiate mvarDecl.type)),