From 43e11f1ba3176c94c7a0a8f78a36da6d70aa0be2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 17 Aug 2024 00:53:38 -0700 Subject: [PATCH] refactor: Always display isInaccessible --- Pantograph/Protocol.lean | 2 +- Pantograph/Serial.lean | 8 ++++---- Test/Common.lean | 1 - Test/Integration.lean | 6 +++--- Test/Metavar.lean | 1 - Test/Proofs.lean | 16 ++++++---------- Test/Tactic/Prograde.lean | 8 ++++---- 7 files changed, 18 insertions(+), 24 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index f954f0d..1a52c8a 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -51,7 +51,7 @@ structure Variable where /-- The name displayed to the user -/ userName: String /-- Does the name contain a dagger -/ - isInaccessible?: Option Bool := .some false + isInaccessible: Bool := false type?: Option Expression := .none value?: Option Expression := .none deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 9f54bbb..c788be2 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -215,13 +215,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName.simpMacroScopes, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { name := ofName fvarId.name, userName := toString userName.simpMacroScopes, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName } let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do match localDecl with @@ -231,7 +231,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) } | .ldecl _ fvarId userName type val _ _ => do @@ -245,7 +245,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName, - isInaccessible? := .some userName.isInaccessibleUserName + isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) value? := value? } diff --git a/Test/Common.lean b/Test/Common.lean index 813e1b3..e572b72 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -138,7 +138,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } diff --git a/Test/Integration.lean b/Test/Integration.lean index 9f7ad92..931c9f2 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -85,14 +85,14 @@ def test_tactic : IO LSpec.TestSeq := let goal1: Protocol.Goal := { name := "_uniq.11", target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, - vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], + vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}], } let goal2: Protocol.Goal := { name := "_uniq.17", target := { pp? := .some "x ∨ y → y ∨ x" }, vars := #[ - { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}, - { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} + { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}, + { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }} ], } subroutine_runner [ diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 65e43a3..2fcab28 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -60,7 +60,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do diff --git a/Test/Proofs.lean b/Test/Proofs.lean index d138e4c..ba97ad7 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -58,7 +58,6 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): @@ -69,7 +68,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O vars := (nameType.map fun x => ({ userName := x.fst, type? := .some { pp? := .some x.snd }, - isInaccessible? := .some false })).toArray } def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do @@ -175,7 +173,6 @@ def test_delta_variable: TestM Unit := do vars := (nameType.map fun x => ({ userName := x.fst, type? := x.snd.map (λ type => { pp? := type }), - isInaccessible? := .some false, })).toArray } @@ -256,9 +253,9 @@ def test_or_comm: TestM Unit := do name := state1g0, target := { pp? := .some "q ∨ p" }, vars := #[ - { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false } + { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } }, + { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } }, + { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } } ] }]) addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome @@ -351,9 +348,9 @@ def test_or_comm: TestM Unit := do userName? := .some caseName, target := { pp? := .some "q ∨ p" }, vars := #[ - { userName := "p", type? := .some typeProp, isInaccessible? := .some false }, - { userName := "q", type? := .some typeProp, isInaccessible? := .some false }, - { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true } + { userName := "p", type? := .some typeProp }, + { userName := "q", type? := .some typeProp }, + { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true } ] } @@ -703,7 +700,6 @@ def test_nat_zero_add_alt: TestM Unit := do name := fvN, userName := "n", type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" }, - isInaccessible? := .some false }], } ]) diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 5b20011..dd194e7 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -82,13 +82,13 @@ def test_proof_eval : TestT Elab.TermElabM Unit := do #[{ target := { pp? := .some "(p ∨ q) ∨ p ∨ q"}, vars := #[ - { userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, - { userName := "h", type? := .some { pp? := .some "p" }, isInaccessible? := .some false }, + { userName := "p", type? := .some { pp? := .some "Prop" } }, + { userName := "q", type? := .some { pp? := .some "Prop" } }, + { userName := "h", type? := .some { pp? := .some "p" } }, { userName := "y", type? := .some { pp? := .some "p ∨ ?m.25" }, value? := .some { pp? := .some "Or.inl h" }, - isInaccessible? := .some false } + } ] }])