Merge pull request 'fix: Printing projection leads to crash' (#37) from io/sexp into dev
Reviewed-on: #37
This commit is contained in:
commit
4871133027
|
@ -86,6 +86,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||||
type := ← serialize_expression state.options info.type,
|
type := ← serialize_expression state.options info.type,
|
||||||
value? := ← value?.mapM (λ v => serialize_expression state.options v),
|
value? := ← value?.mapM (λ v => serialize_expression state.options v),
|
||||||
publicName? := Lean.privateToUserName? name |>.map (·.toString),
|
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,
|
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,
|
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
|
||||||
module? := module?
|
module? := module?
|
||||||
|
|
|
@ -119,7 +119,7 @@ structure LibInspect where
|
||||||
structure LibInspectResult where
|
structure LibInspectResult where
|
||||||
type: Expression
|
type: Expression
|
||||||
value?: Option Expression := .none
|
value?: Option Expression := .none
|
||||||
module?: Option String
|
module?: Option String := .none
|
||||||
-- If the name is private, displays the public facing name
|
-- If the name is private, displays the public facing name
|
||||||
publicName?: Option String := .none
|
publicName?: Option String := .none
|
||||||
typeDependency?: Option (Array String) := .none
|
typeDependency?: Option (Array String) := .none
|
||||||
|
|
|
@ -145,9 +145,9 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
|
||||||
| .proj typeName idx inner => do
|
| .proj typeName idx inner => do
|
||||||
let env ← getEnv
|
let env ← getEnv
|
||||||
let fieldName := getStructureFields env typeName |>.get! idx
|
let fieldName := getStructureFields env typeName |>.get! idx
|
||||||
let inner ← Meta.mkProjection inner fieldName
|
let projectorName := getProjFnForField? env typeName fieldName |>.get!
|
||||||
assert! !inner.isProj
|
let e := Expr.app (.const projectorName []) inner
|
||||||
self inner
|
self e
|
||||||
-- Elides all unhygenic names
|
-- Elides all unhygenic names
|
||||||
binder_info_to_ast : Lean.BinderInfo → String
|
binder_info_to_ast : Lean.BinderInfo → String
|
||||||
| .default => ""
|
| .default => ""
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
{"version": 5,
|
{"version": 6,
|
||||||
"packagesDir": "lake-packages",
|
"packagesDir": "lake-packages",
|
||||||
"packages":
|
"packages":
|
||||||
[{"git":
|
[{"git":
|
||||||
|
@ -8,4 +8,5 @@
|
||||||
"opts": {},
|
"opts": {},
|
||||||
"name": "LSpec",
|
"name": "LSpec",
|
||||||
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
|
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
|
||||||
"inherited": false}}]}
|
"inherited": false}}],
|
||||||
|
"name": "pantograph"}
|
||||||
|
|
Loading…
Reference in New Issue