Merge pull request 'feat: Print structural projection as application' (#35) from io/serial into dev

Reviewed-on: #35
This commit is contained in:
Leni Aniva 2023-12-05 20:20:51 -08:00
commit d846210b9e
2 changed files with 62 additions and 32 deletions

View File

@ -84,67 +84,70 @@ partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
/-- /--
Completely serializes an expression tree. Json not used due to compactness Completely serializes an expression tree. Json not used due to compactness
-/ -/
partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String := partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
self expr self expr
where where
self (e: Expr): String := self (e: Expr): MetaM String :=
match e with match e with
| .bvar deBruijnIndex => | .bvar deBruijnIndex =>
-- This is very common so the index alone is shown. Literals are handled below. -- This is very common so the index alone is shown. Literals are handled below.
-- The raw de Bruijn index should never appear in an unbound setting. In -- The raw de Bruijn index should never appear in an unbound setting. In
-- Lean these are handled using a `#` prefix. -- Lean these are handled using a `#` prefix.
s!"{deBruijnIndex}" pure s!"{deBruijnIndex}"
| .fvar fvarId => | .fvar fvarId =>
let name := of_name fvarId.name let name := of_name fvarId.name
s!"(:fv {name})" pure s!"(:fv {name})"
| .mvar mvarId => | .mvar mvarId =>
let name := of_name mvarId.name let name := of_name mvarId.name
s!"(:mv {name})" pure s!"(:mv {name})"
| .sort level => | .sort level =>
let level := serialize_sort_level_ast level sanitize let level := serialize_sort_level_ast level sanitize
s!"(:sort {level})" pure s!"(:sort {level})"
| .const declName _ => | .const declName _ =>
-- The universe level of the const expression is elided since it should be -- The universe level of the const expression is elided since it should be
-- inferrable from surrounding expression -- inferrable from surrounding expression
s!"(:c {declName})" pure s!"(:c {declName})"
| .app _ _ => | .app _ _ => do
let fn' := self e.getAppFn let fn' self e.getAppFn
let args := e.getAppArgs.map self |>.toList let args := (← e.getAppArgs.mapM self) |>.toList
let args := " ".intercalate args let args := " ".intercalate args
s!"({fn'} {args})" pure s!"({fn'} {args})"
| .lam binderName binderType body binderInfo => | .lam binderName binderType body binderInfo => do
let binderName' := of_name binderName let binderName' := of_name binderName
let binderType' := self binderType let binderType' self binderType
let body' := self body let body' self body
let binderInfo' := binder_info_to_ast binderInfo let binderInfo' := binder_info_to_ast binderInfo
s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
| .forallE binderName binderType body binderInfo => | .forallE binderName binderType body binderInfo => do
let binderName' := of_name binderName let binderName' := of_name binderName
let binderType' := self binderType let binderType' self binderType
let body' := self body let body' self body
let binderInfo' := binder_info_to_ast binderInfo let binderInfo' := binder_info_to_ast binderInfo
s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
| .letE name type value body _ => | .letE name type value body _ => do
-- Dependent boolean flag diacarded -- Dependent boolean flag diacarded
let name' := name_to_ast name let name' := name_to_ast name
let type' := self type let type' self type
let value' := self value let value' self value
let body' := self body let body' self body
s!"(:let {name'} {type'} {value'} {body'})" pure s!"(:let {name'} {type'} {value'} {body'})"
| .lit v => | .lit v =>
-- To not burden the downstream parser who needs to handle this, the literal -- To not burden the downstream parser who needs to handle this, the literal
-- is wrapped in a :lit sexp. -- is wrapped in a :lit sexp.
let v' := match v with let v' := match v with
| .natVal val => toString val | .natVal val => toString val
| .strVal val => s!"\"{val}\"" | .strVal val => s!"\"{val}\""
s!"(:lit {v'})" pure s!"(:lit {v'})"
| .mdata _ inner => | .mdata _ inner =>
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-- It may become necessary to incorporate the metadata. -- It may become necessary to incorporate the metadata.
self inner self inner
| .proj typeName idx struct => | .proj typeName idx inner => do
let struct' := self struct let env ← getEnv
s!"(:proj {typeName} {idx} {struct'})" let fieldName := getStructureFields env typeName |>.get! idx
let inner ← Meta.mkProjection inner fieldName
assert! !inner.isProj
self inner
-- Elides all unhygenic names -- Elides all unhygenic names
binder_info_to_ast : Lean.BinderInfo → String binder_info_to_ast : Lean.BinderInfo → String
| .default => "" | .default => ""
@ -158,7 +161,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
let pp?: Option String := match options.printExprPretty with let pp?: Option String := match options.printExprPretty with
| true => .some pp | true => .some pp
| false => .none | false => .none
let sexp: String := serialize_expression_ast e let sexp: String serialize_expression_ast e
let sexp?: Option String := match options.printExprAST with let sexp?: Option String := match options.printExprAST with
| true => .some sexp | true => .some sexp
| false => .none | false => .none
@ -287,7 +290,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
if options.printContext then if options.printContext then
decl.lctx.fvarIdToDecl.forM printFVar decl.lctx.fvarIdToDecl.forM printFVar
let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) let type_sexp serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
if options.printValue then if options.printValue then
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then

View File

@ -52,7 +52,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let expr := env.find? symbol.toName |>.get! |>.type let expr := env.find? symbol.toName |>.get! |>.type
let test := LSpec.check symbol ((serialize_expression_ast expr) = target) let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let coreM := metaM.run' let coreM := metaM.run'
let coreContext: Core.Context := { let coreContext: Core.Context := {
@ -66,6 +66,32 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "") return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a | .ok a => return a
def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [
("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))")
]
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
let env ← MonadEnv.getEnv
let s := syntax_from_str env source |>.toOption |>.get!
let expr := (← syntax_to_expr s) |>.toOption |>.get!
let test := LSpec.check source ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
let coreContext: Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph/Test>",
fileMap := { source := "", positions := #[0], lines := #[1] }
}
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a
def suite: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules let env: Environment ← importModules
@ -76,6 +102,7 @@ def suite: IO LSpec.TestSeq := do
return LSpec.group "Serialization" $ return LSpec.group "Serialization" $
(LSpec.group "name_to_ast" test_name_to_ast) ++ (LSpec.group "name_to_ast" test_name_to_ast) ++
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++ (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
(LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
(LSpec.group "Sexp from expr" (← test_sexp_of_expr env))
end Pantograph.Test.Serial end Pantograph.Test.Serial