diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 0385cad..b696c25 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -54,18 +54,18 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr | .none, _ => .none -- Information common to all symbols let core := { - type := ← (serialize_expression options info.type).run', + type := ← (serializeExpression options info.type).run', isUnsafe := info.isUnsafe, - value? := ← value?.mapM (λ v => serialize_expression options v |>.run'), + value? := ← value?.mapM (λ v => serializeExpression options v |>.run'), publicName? := Lean.privateToUserName? name |>.map (·.toString), -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. typeDependency? := if args.dependency?.getD false - then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) + then .some <| info.type.getUsedConstants.map (λ n => serializeName n) else .none, valueDependency? := ← if args.dependency?.getD false then info.value?.mapM (λ e => do let e ← unfoldAuxLemmas e - pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) ) + pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) ) else pure (.none), module? := module? } @@ -95,7 +95,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr pure { ctor := rule.ctor.toString, nFields := rule.nfields, - rhs := ← (serialize_expression options rule.rhs).run', + rhs := ← (serializeExpression options rule.rhs).run', }) k := r.k, } } diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index ff365b2..9be86e7 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -144,8 +144,8 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @& try let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr) return .ok { - type := (← serialize_expression options type), - expr := (← serialize_expression options expr) + type := (← serializeExpression options type), + expr := (← serializeExpression options expr) } catch exception => return .error $ errorI "typing" (← exception.toMessageData.toString) @@ -204,9 +204,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto state.restoreMetaM return { root? := ← state.rootExpr?.mapM (λ expr => do - serialize_expression options (← unfoldAuxLemmas expr)), + serializeExpression options (← unfoldAuxLemmas expr)), parent? := ← state.parentExpr?.mapM (λ expr => do - serialize_expression options (← unfoldAuxLemmas expr)), + serializeExpression options (← unfoldAuxLemmas expr)), } diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index ff89222..17618fc 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -18,6 +18,7 @@ structure Options where printExprPretty: Bool := true -- When enabled, print the raw AST of expressions printExprAST: Bool := false + printDependentMVars: Bool := false -- When enabled, the types and values of persistent variables in a goal -- are not shown unless they are new to the proof step. Reduces overhead. -- NOTE: that this assumes the type and assignment of variables can never change. @@ -41,6 +42,7 @@ structure Expression where pp?: Option String := .none -- AST structure sexp?: Option String := .none + dependentMVars?: Option (Array String) := .none deriving Lean.ToJson structure Variable where @@ -182,6 +184,7 @@ structure OptionsSet where printJsonPretty?: Option Bool printExprPretty?: Option Bool printExprAST?: Option Bool + printDependentMVars?: Option Bool noRepeat?: Option Bool printAuxDecls?: Option Bool printImplementationDetailHyps?: Option Bool diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 6c3102f..950818e 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -15,7 +15,7 @@ def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxL namespace Pantograph /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ -def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do +def unfoldAuxLemmas (e : Expr) : CoreM Expr := do Lean.Meta.deltaExpand e Lean.Name.isAuxLemma --- Input Functions --- @@ -43,41 +43,41 @@ def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElab --- Output Functions --- -def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do +def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do Meta.forallTelescope expr fun arr body => do let binders ← arr.mapM fun fvar => do return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType))) return { binders, target := toString (← Meta.ppExpr body) } -def name_to_ast (name: Name) (sanitize: Bool := true): String := +def serializeName (name: Name) (sanitize: Bool := true): String := let internal := name.isInaccessibleUserName || name.hasMacroScopes if sanitize && internal then "_" - else toString name |> enclose_if_escaped + else toString name |> addQuotes where - enclose_if_escaped (n: String) := + addQuotes (n: String) := let quote := "\"" 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 serialize_sort_level_ast (level: Level) (sanitize: Bool): String := +partial def serializeSortLevel (level: Level) (sanitize: Bool): 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 := serialize_sort_level_ast v sanitize - let w := serialize_sort_level_ast w sanitize + let v := serializeSortLevel v sanitize + let w := serializeSortLevel w sanitize s!"(:max {v} {w})" | .imax v w => - let v := serialize_sort_level_ast v sanitize - let w := serialize_sort_level_ast w sanitize + let v := serializeSortLevel v sanitize + let w := serializeSortLevel w sanitize s!"(:imax {v} {w})" | .param name => - let name := name_to_ast name sanitize + let name := serializeName name sanitize s!"{name}" | .mvar id => - let name := name_to_ast id.name sanitize + let name := serializeName id.name sanitize s!"(:mv {name})" match k, u with | 0, _ => u_str @@ -89,7 +89,7 @@ partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String := A `_` symbol in the AST indicates automatic deductions not present in the original expression. -/ -partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do +partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do self expr where self (e: Expr): MetaM String := @@ -100,13 +100,13 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta -- Lean these are handled using a `#` prefix. pure s!"{deBruijnIndex}" | .fvar fvarId => - let name := of_name fvarId.name + let name := ofName fvarId.name pure s!"(:fv {name})" | .mvar mvarId => - let name := of_name mvarId.name + let name := ofName mvarId.name pure s!"(:mv {name})" | .sort level => - let level := serialize_sort_level_ast level sanitize + let level := serializeSortLevel level sanitize pure s!"(:sort {level})" | .const declName _ => -- The universe level of the const expression is elided since it should be @@ -118,20 +118,20 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta let args := " ".intercalate args pure s!"({fn'} {args})" | .lam binderName binderType body binderInfo => do - let binderName' := of_name binderName + let binderName' := ofName binderName let binderType' ← self binderType let body' ← self body - let binderInfo' := binder_info_to_ast binderInfo + let binderInfo' := binderInfoSexp binderInfo pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" | .forallE binderName binderType body binderInfo => do - let binderName' := of_name binderName + let binderName' := ofName binderName let binderType' ← self binderType let body' ← self body - let binderInfo' := binder_info_to_ast binderInfo + let binderInfo' := binderInfoSexp binderInfo pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" | .letE name type value body _ => do -- Dependent boolean flag diacarded - let name' := name_to_ast name + let name' := serializeName name let type' ← self type let value' ← self value let body' ← self body @@ -157,27 +157,31 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta let inner ← self inner pure s!"((:c {projectorName}) {autos} {inner})" -- Elides all unhygenic names - binder_info_to_ast : Lean.BinderInfo → String + binderInfoSexp : Lean.BinderInfo → String | .default => "" | .implicit => " :implicit" | .strictImplicit => " :strictImplicit" | .instImplicit => " :instImplicit" - of_name (name: Name) := name_to_ast name sanitize + ofName (name: Name) := serializeName name sanitize -def serialize_expression (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 | true => pure $ .some $ toString $ ← Meta.ppExpr e | false => pure $ .none let sexp?: Option String ← match options.printExprAST with - | true => pure $ .some $ ← serialize_expression_ast e + | true => pure $ .some $ ← serializeExpressionSexp e + | false => pure $ .none + let dependentMVars? ← match options.printDependentMVars with + | true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString) | false => pure $ .none return { pp?, sexp? + dependentMVars?, } /-- Adapted from ppGoal -/ -def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) +def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) : MetaM Protocol.Goal := do -- Options for printing; See Meta.ppGoal for details let showLetValues := true @@ -191,12 +195,12 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav | .cdecl _ fvarId userName _ _ _ => let userName := userName.simpMacroScopes return { - name := of_name fvarId.name, - userName:= of_name userName.simpMacroScopes, + name := ofName fvarId.name, + userName:= ofName userName.simpMacroScopes, } | .ldecl _ fvarId userName _ _ _ _ => do return { - name := of_name fvarId.name, + name := ofName fvarId.name, userName := toString userName.simpMacroScopes, } let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do @@ -205,24 +209,24 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav let userName := userName.simpMacroScopes let type ← instantiateMVars type return { - name := of_name fvarId.name, - userName:= of_name userName, + name := ofName fvarId.name, + userName:= ofName userName, isInaccessible? := .some userName.isInaccessibleUserName - type? := .some (← serialize_expression options type) + type? := .some (← serializeExpression options type) } | .ldecl _ fvarId userName type val _ _ => do let userName := userName.simpMacroScopes let type ← instantiateMVars type let value? ← if showLetValues then let val ← instantiateMVars val - pure $ .some (← serialize_expression options val) + pure $ .some (← serializeExpression options val) else pure $ .none return { - name := of_name fvarId.name, - userName:= of_name userName, + name := ofName fvarId.name, + userName:= ofName userName, isInaccessible? := .some userName.isInaccessibleUserName - type? := .some (← serialize_expression options type) + type? := .some (← serializeExpression options type) value? := value? } let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do @@ -238,14 +242,14 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav | false => ppVar localDecl return var::acc return { - name := of_name goal.name, - userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName), + name := ofName goal.name, + userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, - target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), + target := (← serializeExpression options (← instantiateMVars mvarDecl.type)), vars := vars.reverse.toArray } where - of_name (n: Name) := name_to_ast n (sanitize := false) + ofName (n: Name) := serializeName n (sanitize := false) protected def GoalState.serializeGoals (state: GoalState) @@ -258,12 +262,12 @@ protected def GoalState.serializeGoals goals.mapM fun goal => do match state.mctx.findDecl? goal with | .some mvarDecl => - let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?) + let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?) pure serializedGoal | .none => throwError s!"Metavariable does not exist in context {goal.name}" /-- Print the metavariables in a readable format -/ -protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do +protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do goalState.restoreMetaM let savedState := goalState.savedState let goals := savedState.tactic.goals @@ -298,7 +302,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag let type ← if options.instantiate then instantiateMVars decl.type else pure $ decl.type - let type_sexp ← serialize_expression_ast type (sanitize := false) + let type_sexp ← serializeExpressionSexp 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/Test/Metavar.lean b/Test/Metavar.lean index eff2103..33fe8cb 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -28,7 +28,7 @@ def test_instantiate_mvar: TestM Unit := do addTest $ assertUnreachable e return () let t ← Lean.Meta.inferType expr - addTest $ LSpec.check "typing" ((toString (← serialize_expression_ast t)) = + addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) = "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))") return () @@ -121,8 +121,12 @@ def test_m_couple_simp: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = + let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true }) + addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) = #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) + addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) = + #[#["_uniq.38"], #["_uniq.38"], #[]]) + let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with | .success state => pure state | other => do @@ -245,8 +249,8 @@ def test_partial_continuation: TestM Unit := do -- Roundtrip --let coupled_goals := coupled_goals.map (λ g => - -- { name := str_to_name $ name_to_ast g.name (sanitize := false)}) - let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false)) + -- { name := str_to_name $ serializeName g.name (sanitize := false)}) + let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false)) let coupled_goals := coupled_goals.map (λ g => { name := g.toName }) let state1b ← match state2.resume (goals := coupled_goals) with | .error msg => do diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 1b1b9de..a3201a2 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -229,7 +229,7 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone - let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false) + let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) -- This is due to delayed assignment addTest $ LSpec.test "(2 parent)" (state2parent == "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") @@ -239,7 +239,7 @@ def test_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false) + let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false) addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with @@ -248,7 +248,7 @@ def test_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty - let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false) + let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false) addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)") addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with diff --git a/Test/Serial.lean b/Test/Serial.lean index e9f4d85..f55c18f 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -10,13 +10,13 @@ open Pantograph deriving instance Repr, DecidableEq for Protocol.BoundExpression -def test_name_to_ast: LSpec.TestSeq := +def test_serializeName: LSpec.TestSeq := let quote := "\"" let escape := "\\" - LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++ - LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++ + LSpec.test "a.b.1" (serializeName (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++ + LSpec.test "seg.«a.b»" (serializeName (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++ -- Pathological test case - LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}") + LSpec.test s!"«̈{escape}{quote}»" (serializeName (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}") def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Protocol.BoundExpression) := [ @@ -26,7 +26,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do runCoreMSeq env $ entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv let expr := env.find? symbol |>.get! |>.type - let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target) + let test := LSpec.check symbol.toString ((← typeExprToBound expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run' def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do @@ -43,7 +43,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do runMetaMSeq env $ entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv let expr := env.find? symbol.toName |>.get! |>.type - let test := LSpec.check symbol ((← serialize_expression_ast expr) = target) + let test := LSpec.check symbol ((← serializeExpressionSexp expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do @@ -61,7 +61,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do let expr ← match (← elabTerm s) with | .ok expr => pure expr | .error e => return elabFailure e - let test := LSpec.check source ((← serialize_expression_ast expr) = target) + let test := LSpec.check source ((← serializeExpressionSexp expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext) @@ -80,7 +80,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do let env ← MonadEnv.getEnv let testCaseName := target.take 10 - let test := LSpec.check testCaseName ((← serialize_expression_ast expr) = target) + let test := LSpec.check testCaseName ((← serializeExpressionSexp expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext) @@ -95,7 +95,7 @@ def test_instance (env: Environment): IO LSpec.TestSeq := def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ - ("name_to_ast", do pure test_name_to_ast), + ("serializeName", do pure test_serializeName), ("Expression binder", test_expr_to_binder env), ("Sexp from symbol", test_sexp_of_symbol env), ("Sexp from elaborated expr", test_sexp_of_elab env),