aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

feat: Simplify sexp printing #149

Open
aniva wants to merge 3 commits from delate/sexp into dev
pull from: delate/sexp
merge into: aniva:dev
Conversation 0 Commits 3 Files Changed 3 +22 -22
3 changed files with 22 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
Pantograph/Delate.lean
View File

@ -264,25 +264,24 @@ def serializeName (name: Name) (sanitize: Bool := true): String :=
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n 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)` -/ /-- 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 k := level.getOffset
let u := level.getLevelOffset let u := level.getLevelOffset
let u_str := match u with let u_str := match u with
| .zero => "0" | .zero => "0"
| .succ _ => panic! "getLevelOffset should not return .succ" | .succ _ => panic! "getLevelOffset should not return .succ"
| .max v w => | .max v w =>
let v := serializeSortLevel v sanitize let v := serializeSortLevel v
let w := serializeSortLevel w sanitize let w := serializeSortLevel w
s!"(:max {v} {w})" s!"(:max {v} {w})"
| .imax v w => | .imax v w =>
let v := serializeSortLevel v sanitize let v := serializeSortLevel v
let w := serializeSortLevel w sanitize let w := serializeSortLevel w
s!"(:imax {v} {w})" s!"(:imax {v} {w})"
| .param name => | .param name =>
let name := serializeName name sanitize
s!"{name}" s!"{name}"
| .mvar id => | .mvar id =>
let name := serializeName id.name sanitize let name := id.name
s!"(:mv {name})" s!"(:mv {name})"
match k, u with match k, u with
| 0, _ => u_str | 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. 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 self expr
where where
delayedMVarToSexp (e: Expr): MetaM (Option String) := do delayedMVarToSexp (e: Expr): MetaM (Option String) := do
@ -334,9 +333,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
let name := mvarId.name let name := mvarId.name
pure s!"(:{pref} {name})" pure s!"(:{pref} {name})"
| .sort level => | .sort level =>
let level := serializeSortLevel level sanitize let level := serializeSortLevel level
pure s!"(:sort {level})" pure s!"(:sort {level})"
| .const declName _ => | .const declName _ =>
let declName := serializeName declName (sanitize := false)
-- The universe level of the const expression is elided since it should be -- The universe level of the const expression is elided since it should be
-- inferrable from surrounding expression -- inferrable from surrounding expression
pure s!"(:c {declName})" pure s!"(:c {declName})"
@ -369,7 +369,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
-- is wrapped in a :lit sexp. -- is wrapped in a :lit sexp.
let v' := match v with let v' := match v with
| .natVal val => toString val | .natVal val => toString val
| .strVal val => s!"\"{val}\"" | .strVal val => IR.EmitC.quoteString val
pure s!"(:lit {v'})" pure s!"(:lit {v'})"
| .mdata _ inner => | .mdata _ inner =>
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
@ -384,9 +384,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
-- Elides all unhygenic names -- Elides all unhygenic names
binderInfoSexp : Lean.BinderInfo → String binderInfoSexp : Lean.BinderInfo → String
| .default => "" | .default => ""
| .implicit => " :implicit" | .implicit => " :i"
| .strictImplicit => " :strictImplicit" | .strictImplicit => " :si"
| .instImplicit => " :instImplicit" | .instImplicit => " :ii"
def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
let pp?: Option String ← match options.printExprPretty with let pp?: Option String ← match options.printExprPretty with
@ -532,7 +532,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
then instantiateAll decl.type then instantiateAll decl.type
else pure $ decl.type else pure $ decl.type
let type_sexp ← if options.printSexp then let type_sexp ← if options.printSexp then
let sexp ← serializeExpressionSexp type (sanitize := false) let sexp ← serializeExpressionSexp type
pure <| " " ++ sexp pure <| " " ++ sexp
else else
pure "" pure ""

8
Test/Delate.lean
View File

@ -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)))"), ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
-- These ones are normal and easy -- 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.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 -- Handling of higher order types
("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"), ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))") ("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) := [ 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: 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))"), ("λ 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)"), ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"), ("λ {α} => 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)))"), ("(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) => entries.foldlM (λ suites (source, levels, target) =>
@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
.default) .default)
.implicit) .implicit)
.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 let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do

8
Test/Proofs.lean
View File

@ -97,7 +97,7 @@ def test_identity: TestM Unit := do
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) = addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
#[inner]) #[inner])
let state1parent ← state1.withParentContext do 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)))") addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
-- Individual test cases -- Individual test cases
@ -259,7 +259,7 @@ def test_or_comm: TestM Unit := do
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
let state1parent ← state1.withParentContext do 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))))") 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 tactic := "cases h"
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with 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 addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state2parent ← state2.withParentContext do 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 orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" 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}))" 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 addTest $ assertUnreachable $ other.toString
return () return ()
let state3_1parent ← state3_1.withParentContext do 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.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) addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with