aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 3 Packages Projects Releases 1 Wiki Activity

refactor: Remove sanitization for mvarId/fvarId

This commit is contained in:
Leni Aniva 2024-11-26 12:57:19 -08:00
parent a8e7a1a726
commit 44aef76a10
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 7 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Pantograph/Delate.lean
View File

@ -327,11 +327,11 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
-- Lean these are handled using a `#` prefix. -- Lean these are handled using a `#` prefix.
pure s!"{deBruijnIndex}" pure s!"{deBruijnIndex}"
| .fvar fvarId => | .fvar fvarId =>
let name := ofName fvarId.name let name := fvarId.name
pure s!"(:fv {name})" pure s!"(:fv {name})"
| .mvar mvarId => do | .mvar mvarId => do
let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv" let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
let name := ofName 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 sanitize
@ -387,7 +387,6 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
| .implicit => " :implicit" | .implicit => " :implicit"
| .strictImplicit => " :strictImplicit" | .strictImplicit => " :strictImplicit"
| .instImplicit => " :instImplicit" | .instImplicit => " :instImplicit"
ofName (name: Name) := serializeName name sanitize
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
@ -420,13 +419,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
match localDecl with match localDecl with
| .cdecl _ fvarId userName _ _ _ => | .cdecl _ fvarId userName _ _ _ =>
return { return {
name := ofName fvarId.name, name := fvarId.name.toString,
userName:= ofName userName.simpMacroScopes, userName:= ofName userName.simpMacroScopes,
isInaccessible := userName.isInaccessibleUserName isInaccessible := userName.isInaccessibleUserName
} }
| .ldecl _ fvarId userName _ _ _ _ => do | .ldecl _ fvarId userName _ _ _ _ => do
return { return {
name := ofName fvarId.name, name := fvarId.name.toString,
userName := toString userName.simpMacroScopes, userName := toString userName.simpMacroScopes,
isInaccessible := userName.isInaccessibleUserName isInaccessible := userName.isInaccessibleUserName
} }
@ -436,7 +435,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
let userName := userName.simpMacroScopes let userName := userName.simpMacroScopes
let type ← instantiate type let type ← instantiate type
return { return {
name := ofName fvarId.name, name := fvarId.name.toString,
userName:= ofName userName, userName:= ofName userName,
isInaccessible := userName.isInaccessibleUserName isInaccessible := userName.isInaccessibleUserName
type? := .some (← serializeExpression options type) type? := .some (← serializeExpression options type)
@ -450,7 +449,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
else else
pure $ .none pure $ .none
return { return {
name := ofName fvarId.name, name := fvarId.name.toString,
userName:= ofName userName, userName:= ofName userName,
isInaccessible := userName.isInaccessibleUserName isInaccessible := userName.isInaccessibleUserName
type? := .some (← serializeExpression options type) type? := .some (← serializeExpression options type)
@ -469,7 +468,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
| false => ppVar localDecl | false => ppVar localDecl
return var::acc return var::acc
return { return {
name := ofName goal.name, name := goal.name.toString,
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
isConversion := isLHSGoal? mvarDecl.type |>.isSome, isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serializeExpression options (← instantiate mvarDecl.type)), target := (← serializeExpression options (← instantiate mvarDecl.type)),