From 0ecfa9fc261b53c2e046004ea4c82bf09254826e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 25 Oct 2023 22:18:59 -0700 Subject: [PATCH] feat: Display user name in Goal structure 1. Modify `serialize_expression_ast` so its no longer a monad 2. Test existence of root expression --- Pantograph/Goal.lean | 9 +++++++-- Pantograph/Protocol.lean | 5 ++++- Pantograph/Serial.lean | 42 ++++++++++++++++++++++------------------ Test/Common.lean | 19 ++++++++++++++++++ Test/Proofs.lean | 25 ++++++++++++------------ Test/Serial.lean | 4 ++-- 6 files changed, 68 insertions(+), 36 deletions(-) create mode 100644 Test/Common.lean diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 3f42abe..4e57134 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -143,7 +143,12 @@ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Excep } protected def GoalState.rootExpr (goalState: GoalState): Option Expr := - goalState.mctx.eAssignment.find? goalState.root |>.filter (λ e => ¬ e.hasMVar) + let expr := goalState.mctx.eAssignment.find! goalState.root + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + if expr.hasMVar then + .none + else + .some expr -- Diagnostics functions @@ -183,7 +188,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrin printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do if options.printContext then decl.lctx.fvarIdToDecl.forM printFVar - let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) + let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" if options.printValue then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 49103d7..a6bae29 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -43,7 +43,10 @@ structure Expression where deriving Lean.ToJson structure Variable where - name: String + /-- The internal name used in raw expressions -/ + name: String := "" + /-- The name displayed to the user -/ + userName: String /-- Does the name contain a dagger -/ isInaccessible?: Option Bool := .none type?: Option Expression := .none diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index a5acd7f..99f95ef 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -102,8 +102,8 @@ def serialize_sort_level_ast (level: Level): String := /-- Completely serializes an expression tree. Json not used due to compactness -/ -def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do - return self expr +def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String := + self expr where self (e: Expr): String := match e with @@ -175,7 +175,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E let pp?: Option String := match options.printExprPretty with | true => .some pp | false => .none - let sexp: String := (← serialize_expression_ast e) + let sexp: String := serialize_expression_ast e let sexp?: Option String := match options.printExprAST with | true => .some sexp | false => .none @@ -196,27 +196,30 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe Meta.withLCtx lctx mvarDecl.localInstances do let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do match localDecl with - | .cdecl _ _ varName _ _ _ => - let varName := varName.simpMacroScopes + | .cdecl _ fvarId userName _ _ _ => + let userName := userName.simpMacroScopes return { - name := toString varName, + name := of_name fvarId.name, + userName:= of_name userName.simpMacroScopes, } - | .ldecl _ _ varName _ _ _ _ => do + | .ldecl _ fvarId userName _ _ _ _ => do return { - name := toString varName, + name := of_name fvarId.name, + userName := toString userName.simpMacroScopes, } let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do match localDecl with - | .cdecl _ _ varName type _ _ => - let varName := varName.simpMacroScopes + | .cdecl _ fvarId userName type _ _ => + let userName := userName.simpMacroScopes let type ← instantiateMVars type return { - name := toString varName, - isInaccessible? := .some varName.isInaccessibleUserName + name := of_name fvarId.name, + userName:= of_name userName, + isInaccessible? := .some userName.isInaccessibleUserName type? := .some (← serialize_expression options type) } - | .ldecl _ _ varName type val _ _ => do - let varName := varName.simpMacroScopes + | .ldecl _ fvarId userName type val _ _ => do + let userName := userName.simpMacroScopes let type ← instantiateMVars type let value? ← if showLetValues then let val ← instantiateMVars val @@ -224,8 +227,9 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe else pure $ .none return { - name := toString varName, - isInaccessible? := .some varName.isInaccessibleUserName + name := of_name fvarId.name, + userName:= of_name userName, + isInaccessible? := .some userName.isInaccessibleUserName type? := .some (← serialize_expression options type) value? := value? } @@ -242,13 +246,13 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe | false => ppVar localDecl return var::acc return { - caseName? := match mvarDecl.userName with - | Name.anonymous => .none - | name => .some <| toString name, + caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), vars := vars.reverse.toArray } + where + of_name (n: Name) := name_to_ast n (sanitize := false) diff --git a/Test/Common.lean b/Test/Common.lean new file mode 100644 index 0000000..3e52932 --- /dev/null +++ b/Test/Common.lean @@ -0,0 +1,19 @@ +import Pantograph.Protocol + +namespace Pantograph + +namespace Protocol +/-- Set internal names to "" -/ +def Goal.devolatilize (goal: Goal): Goal := + { + goal with + vars := goal.vars.map removeInternalAux, + } + where removeInternalAux (v: Variable): Variable := + { + v with + name := "" + } +end Protocol + +end Pantograph diff --git a/Test/Proofs.lean b/Test/Proofs.lean index ac9c78c..d609dd4 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -4,6 +4,7 @@ Tests pertaining to goals with no interdependencies import LSpec import Pantograph.Goal import Pantograph.Serial +import Test.Common namespace Pantograph @@ -69,7 +70,7 @@ def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goa { target := { pp? := .some target}, vars := (nameType.map fun x => ({ - name := x.fst, + userName := x.fst, type? := .some { pp? := .some x.snd }, isInaccessible? := .some false })).toArray @@ -79,7 +80,7 @@ def buildGoalSelective (nameType: List (String × Option String)) (target: Strin { target := { pp? := .some target}, vars := (nameType.map fun x => ({ - name := x.fst, + userName := x.fst, type? := x.snd.map (λ type => { pp? := type }), isInaccessible? := x.snd.map (λ _ => false) })).toArray @@ -104,7 +105,6 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := | .ok (_, a) => return a - -- Individual test cases example: ∀ (a b: Nat), a + b = b + a := by intro n m @@ -125,7 +125,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "intro n m" (goal1 = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n") + addTest $ LSpec.check "intro n m" (goal1.devolatilize = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n") match ← state1.execute (goalId := 0) (tactic := "assumption") with | .failure #[message] => @@ -170,14 +170,14 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "p q h" (goal1 = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p") + addTest $ LSpec.check "p q h" (goal1.devolatilize = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p") let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with | .success state #[goal1, goal2] => pure (state, goal1, goal2) | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "cases h/1" (goal1 = branchGoal "inl" "p") - addTest $ LSpec.check "cases h/2" (goal2 = branchGoal "inr" "q") + addTest $ LSpec.check "cases h/1" (goal1.devolatilize = branchGoal "inl" "p") + addTest $ LSpec.check "cases h/2" (goal2.devolatilize = branchGoal "inr" "q") let (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with | .success state #[goal] => pure (state, goal) @@ -200,6 +200,7 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () + addTest $ LSpec.check "4_2 root" state4_2.rootExpr.isNone -- Ensure the proof can continue from `state4_2`. let state2b ← match state2.continue state4_2 with | .error msg => do @@ -217,8 +218,8 @@ def proof_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - IO.println "===== 4_1 =====" - state4_1.print ({ printNonVisible := false }) + state4_1.print + addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome return () where @@ -227,9 +228,9 @@ def proof_or_comm: TestM Unit := do caseName? := .some caseName, target := { pp? := .some "q ∨ p" }, vars := #[ - { name := "p", type? := .some typeProp, isInaccessible? := .some false }, - { name := "q", type? := .some typeProp, isInaccessible? := .some false }, - { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } + { userName := "p", type? := .some typeProp, isInaccessible? := .some false }, + { userName := "q", type? := .some typeProp, isInaccessible? := .some false }, + { userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } ] } diff --git a/Test/Serial.lean b/Test/Serial.lean index 30d6f60..9a42992 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -47,8 +47,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv let expr := str_to_name symbol |> env.find? |>.get! |>.type - let test := LSpec.check symbol ((← serialize_expression_ast expr) = target) - return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run' + let test := LSpec.check symbol ((serialize_expression_ast expr) = target) + return LSpec.TestSeq.append suites test) LSpec.TestSeq.done let coreM := metaM.run' let coreContext: Core.Context := { currNamespace := Lean.Name.str .anonymous "Aniva"