From c0090dec975cd30303060f172ec1da28782e53ad Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 15 Dec 2024 12:40:47 -0800 Subject: [PATCH 1/3] fix: Quote string literal in sexp --- Pantograph/Delate.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 4b3bd51..582b783 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -369,7 +369,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM -- is wrapped in a :lit sexp. let v' := match v with | .natVal val => toString val - | .strVal val => s!"\"{val}\"" + | .strVal val => IR.EmitC.quoteString val pure s!"(:lit {v'})" | .mdata _ inner => -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- 2.44.1 From 7a3b89cc0edcb223ddaf23ff2f35c3fa14dfb3bd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 15 Dec 2024 12:48:49 -0800 Subject: [PATCH 2/3] feat: Simplify sexp binder --- Pantograph/Delate.lean | 6 +++--- Test/Delate.lean | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 582b783..c68d7cd 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -384,9 +384,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM -- Elides all unhygenic names binderInfoSexp : Lean.BinderInfo → String | .default => "" - | .implicit => " :implicit" - | .strictImplicit => " :strictImplicit" - | .instImplicit => " :instImplicit" + | .implicit => " :i" + | .strictImplicit => " :si" + | .instImplicit => " :ii" def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp?: Option String ← match options.printExprPretty with diff --git a/Test/Delate.lean b/Test/Delate.lean index d918dc8..013be73 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -35,7 +35,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do ("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)"), + ("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)) :i) :i)"), -- Handling of higher order types ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"), ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))") @@ -50,8 +50,8 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do let entries: List (String × (List Name) × String) := [ ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"), ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), - ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), - ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"), + ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"), + ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"), ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"), ] entries.foldlM (λ suites (source, levels, target) => @@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do .default) .implicit) .implicit, - "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)" + "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)" ), ] let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do -- 2.44.1 From 53bad1c4c995ee44f145439add930177ac49f16f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 15 Dec 2024 12:52:08 -0800 Subject: [PATCH 3/3] refactor: Remove obsolete sanitize option --- Pantograph/Delate.lean | 20 ++++++++++---------- Test/Proofs.lean | 8 ++++---- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index c68d7cd..38d8bda 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -264,25 +264,24 @@ def serializeName (name: Name) (sanitize: Bool := true): String := if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/ -partial def serializeSortLevel (level: Level) (sanitize: Bool): String := +partial def serializeSortLevel (level: Level) : String := let k := level.getOffset let u := level.getLevelOffset let u_str := match u with | .zero => "0" | .succ _ => panic! "getLevelOffset should not return .succ" | .max v w => - let v := serializeSortLevel v sanitize - let w := serializeSortLevel w sanitize + let v := serializeSortLevel v + let w := serializeSortLevel w s!"(:max {v} {w})" | .imax v w => - let v := serializeSortLevel v sanitize - let w := serializeSortLevel w sanitize + let v := serializeSortLevel v + let w := serializeSortLevel w s!"(:imax {v} {w})" | .param name => - let name := serializeName name sanitize s!"{name}" | .mvar id => - let name := serializeName id.name sanitize + let name := id.name s!"(:mv {name})" match k, u with | 0, _ => u_str @@ -295,7 +294,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String := A `_` symbol in the AST indicates automatic deductions not present in the original expression. -/ -partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do +partial def serializeExpressionSexp (expr: Expr) : MetaM String := do self expr where delayedMVarToSexp (e: Expr): MetaM (Option String) := do @@ -334,9 +333,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM let name := mvarId.name pure s!"(:{pref} {name})" | .sort level => - let level := serializeSortLevel level sanitize + let level := serializeSortLevel level pure s!"(:sort {level})" | .const declName _ => + let declName := serializeName declName (sanitize := false) -- The universe level of the const expression is elided since it should be -- inferrable from surrounding expression pure s!"(:c {declName})" @@ -532,7 +532,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState : then instantiateAll decl.type else pure $ decl.type let type_sexp ← if options.printSexp then - let sexp ← serializeExpressionSexp type (sanitize := false) + let sexp ← serializeExpressionSexp type pure <| " " ++ sexp else pure "" diff --git a/Test/Proofs.lean b/Test/Proofs.lean index a6b5487..104a849 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -97,7 +97,7 @@ def test_identity: TestM Unit := do addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) = #[inner]) let state1parent ← state1.withParentContext do - serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false) + serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))") -- Individual test cases @@ -259,7 +259,7 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone let state1parent ← state1.withParentContext do - serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false) + serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))") let tactic := "cases h" let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with @@ -276,7 +276,7 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone let state2parent ← state2.withParentContext do - serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) + serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" @@ -292,7 +292,7 @@ def test_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () let state3_1parent ← state3_1.withParentContext do - serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false) + serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with -- 2.44.1