fix: Printing projection leads to crash #37

Merged
aniva merged 2 commits from io/sexp into dev 2023-12-07 12:33:02 -08:00
4 changed files with 8 additions and 6 deletions

View File

@ -86,6 +86,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
type := ← serialize_expression state.options info.type,
value? := ← value?.mapM (λ v => serialize_expression state.options v),
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) else .none,
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
module? := module?

View File

@ -119,7 +119,7 @@ structure LibInspect where
structure LibInspectResult where
type: Expression
value?: Option Expression := .none
module?: Option String
module?: Option String := .none
-- If the name is private, displays the public facing name
publicName?: Option String := .none
typeDependency?: Option (Array String) := .none

View File

@ -145,9 +145,9 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
| .proj typeName idx inner => do
let env ← getEnv
let fieldName := getStructureFields env typeName |>.get! idx
let inner ← Meta.mkProjection inner fieldName
assert! !inner.isProj
self inner
let projectorName := getProjFnForField? env typeName fieldName |>.get!
let e := Expr.app (.const projectorName []) inner
self e
-- Elides all unhygenic names
binder_info_to_ast : Lean.BinderInfo → String
| .default => ""

View File

@ -1,4 +1,4 @@
{"version": 5,
{"version": 6,
"packagesDir": "lake-packages",
"packages":
[{"git":
@ -8,4 +8,5 @@
"opts": {},
"name": "LSpec",
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
"inherited": false}}]}
"inherited": false}}],
"name": "pantograph"}