feat: Option to collect dependent metavariables #69
|
@ -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,
|
||||
} }
|
||||
|
|
|
@ -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)),
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -49,7 +49,7 @@ def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := 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
|
||||
|
@ -59,25 +59,25 @@ def name_to_ast (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 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 :=
|
||||
|
@ -106,7 +106,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
|
|||
let name := of_name 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
|
||||
|
@ -131,7 +131,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
|
|||
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
|
||||
|
@ -162,14 +162,14 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
|
|||
| .implicit => " :implicit"
|
||||
| .strictImplicit => " :strictImplicit"
|
||||
| .instImplicit => " :instImplicit"
|
||||
of_name (name: Name) := name_to_ast name sanitize
|
||||
of_name (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
|
||||
return {
|
||||
pp?,
|
||||
|
@ -177,7 +177,7 @@ def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol
|
|||
}
|
||||
|
||||
/-- 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
|
||||
|
@ -208,21 +208,21 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
|
|||
name := of_name fvarId.name,
|
||||
userName:= of_name 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,
|
||||
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
|
||||
|
@ -241,11 +241,11 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
|
|||
name := of_name goal.name,
|
||||
userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name 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)
|
||||
of_name (n: Name) := serializeName n (sanitize := false)
|
||||
|
||||
protected def GoalState.serializeGoals
|
||||
(state: GoalState)
|
||||
|
@ -258,7 +258,7 @@ 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}"
|
||||
|
||||
|
@ -298,7 +298,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
|
||||
|
|
|
@ -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 ()
|
||||
|
||||
|
@ -245,8 +245,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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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) := [
|
||||
|
@ -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),
|
||||
|
|
Loading…
Reference in New Issue